Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint
Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.
Code (1)
Tasks
Automated Theorem ProvingTranslationSimilar Papers 제목 키워드 기반
Solving Quantified Modal Logic Problems by Translation to Classical Logics
This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-o…
Automated Theorem ProvingTranslationLearning-Assisted Automated Reasoning with Flyspeck
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machine-learning premise selection methods trained on the proofs, producing an AI sys…
CPUThe Isabelle ENIGMA
We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of t…
Automated Theorem ProvingSubtyping in DHOL -- Extended preprint
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantl…
Automated Theorem ProvingGraph Representations for Higher-Order Logic and Theorem Proving
This paper presents the first use of graph neural networks (GNNs) for higher-order proof search and demonstrates that GNNs can improve upon state-of-the-art results in this domain. Interactive, higher-order theorem prove…
Automated Theorem Proving