중첩 미적분학

중첩 미적분은 등가 1차 논리에서의 추리를 위한 미적분이다.1990년대 초에 개발되었으며, 크누스-벤딕스 완성의 맥락에서 개발된 1차 결의안으로부터의 개념과 주문 기반 평등 취급의 개념을 결합한다.결의(정확한 논리)나 변함없는 완료(완전한 폐쇄 논리로)의 일반화라고 볼 수 있다.대부분의 1차분산술로서, 중첩은 1차분 절의 집합의 만족도를 나타내려고 한다. 즉, 재삽입으로 증거를 수행한다.중첩은 반박-완전하다. 무한한 자원과 공정한 파생 전략을 고려할 때, 어떤 불만족스러운 조항에서든 모순은 결국 도출될 것이다.

2007년 현재, 1차 논리를 위한 (최첨단) 정리 추진기의 대부분은 순수 미적분을 구현하는 소수만이지만, 중첩(예: E 등가 정리 프로베라)에 기초하고 있다.