Equality and extensionality in automated higher order theorem proving
Equality and extensionality in automated higher order theorem proving
复制标题
自动高阶定理证明中的等式和外延性
DOI：
10.22028/d291-25680
复制
发表时间：
1999
影响因子：
1.3
通讯作者：
Christoph Benzmüller
中科院分区：
文献类型：
--
作者：
Christoph Benzmüller
本文主要研究基于丘奇单型λ演算（经典类型论）的高阶定理自动证明中的等式性和可扩展性。首先，由平等在其中所扮演的不同角色所激发的各种语义概念的景观被阻止。这一领域中的每一个语义概念——包括亨金语义——都与一个抽象的一致性原则联系在一起，该原则可用于分析高阶微积分的语法和语义之间的联系。除了这些证明理论工具之外，这方面的主要贡献是三个新的演算ER（扩展高阶分辨率），EP（扩展高阶调节）和ERUE（扩展高阶正则-分辨率），它们改进了经典类型理论中定义和原始相等的机械化。与迄今为止发展的经典类型论的反驳方法相反，这些演算不需要额外的延展性公理就能达到亨金完备性。关键思想是允许从高阶统一到整体反驳搜索的递归调用。与EP和ERUE相比，微积分ER只将等式视为一个定义的概念，它已经在定理证明器LEO中实现，并且在一个案例研究中证明了这种方法对于证明关于集合的简单定理的适用性。
This thesis focuses on equality and extensionality in automated higher-order theorem proving based on Church's simply typed lambda - calculus (classical type theory). First, a landscape of various semantical notions is preented that is motivated by the different roles equality adopts in them. Each of the semantical notions in this landscape - including Henkin semantics - is then linked with an abstract consistency principle that can be employed for analysing the connection between syntax and semantics of higer-order calculi. Apart from this proof theoretic tools, the main contributions of this are the three new calculi ER (extensional higher-order resolution), EP (extensoinal higher-order paramodulation) and ERUE (extensonal higher-order RUE-resolution) which improve the mechanisation of defined and primitvie equality in classical type theory. In contrast to the refutation approaches for classical type theory developed so far, these calculi reach Henkin completeness without requiring additional extensionality axioms. The key idea is to allow for recursive calls from higer-order unification to the overall refutation search. Calculus ER, which in contrast to EP and ERUE, considers equality only as a defined notion, has been implemented in the theorem prover LEO and the suitability of this approach for proving simple theorems about sets has been demonstrated in a case study.
Diese Arbeit untersucht Gleichheit und Extensionalitaet im automatischen Beweisen in Logik hoeherer Stufe. Die betrachtete Sprache ist die klassische Typtheorie, d.h. eine Logik hoeherer Stufe basierend auf Churchs einfach getypten Lambda-Kalkul. Zunachst werden unterschiedlich starke Semantikbegriffe fur die klassische Typtheorie erarbeitet, die durch die jeweils unterschiedlichen Rollen, die die Gleichheit in ihnen einnimmt, motiviert sind. Jedem der eingefuhrten Semantikbegriffe wird dann eine Menge abstrakter Konsistenzeigenschaften zugeordnet mit dem Ziel, die Analyse der Verbindung zwischen Syntax und Semantik von Beweiskalkulen fur die klassische Typtheorie zu erleichtern.