3
$\begingroup$

I'm wondering how much overlap (read: code-reusage) there is between a PA and an ATP system.

Are they based upon the same type system at least?

I'm wondering, because right now I'm working on implemenation exercises from Pierce's Types & Programming Languages book, which is geared toward PA's, but I also have an interest in ATP - automated theorem proving. It would be nice if the base system were or could be the exact same thing.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

Unfortunately there is much less code reuse possible than one would hope.

There three levels to consider:

  1. Differences between mathematical foundations (and implementations) between proof assistants.
  2. Differences between mathematical foundations (and implementations) between automated theorem provers.
  3. Differences between the approaches taken to develop a proof assistant and an automated theorem prover.

One would hope that at least for 1. and 2. the code should be reusable, but it very much depends on the mathematical foundation chosen for the PA (or ATP). For instance, Coq is based on the type theory called Calculus of Inductive constructions, while Agda is based on Martin-Löf type theory - this means that proofs may not be fundamentally compatible (i.e. a theorem may hold in one type theory, but not in the other), let alone the fact that Coq and Agda use very different syntax (making actual code reuse infeasible). There are steps being taken towards translating proofs from different foundations (for instance [1], [2]), but there is a lot to be said there. A similar problem occurs in ATPs, although there at least the input format (specification of a conjecture to be proven) is somewhat standardised, mostly they use the TPTP format [3] (and the TSTP format for proofs).

For 3. (differences between ATPs and PAs), there is the problem, that ATPs and PAs are addressing a different problem: while proof assistants aim to check proofs, automated theorem provers aim to automate producing proofs. For this reason, most PAs are based on type-theory (dependent types enable better expressivity for the problems at hand), while ATPs are mostly dealing with first-order logic, or "simple theories" (linear arithmetic, theory of arrays etc.) supported by SMT solvers - theories where we can reason by refutation and the currently available automation techniques (tableaux method, superposition calculus, ...) can be used. However, there are projects aiming towards importing proofs produced by ATPs (usually the TSTP trace) into some proof assistants for re-checking, for instance Ekstrakto [4,5] and TESC [6,7].

[1] The Dedukti logical framework: https://deducteam.github.io

[2] Anja Petković Komel: Meta-analysis of type theories with an application to the design of formal proofs, PhD thesis, University of Ljubljana, 2021. URL: https://anjapetkovic.com/img/doctoralThesis.pdf

[3] Thousands of Problems for Theorem Provers: https://www.tptp.org/

[4] Yacine El Haddad. Integrating Automated Theorem Provers in Proof Assistants. PhD thesis, Université Paris-Saclay, 2021.

[5] Ekstrakto URL: https://github.com/Deducteam/ekstrakto

[6] Seulkee Baek. A Formally Verified Checker for First-Order Proofs. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving (ITP 2021), volume 193 of Leibniz International Proceed- ings in Informatics (LIPIcs), pages 6:1–6:13, Dagstuhl, Germany, 2021. Schloss Dagstuhl – Leibniz-Zentrum für Informatik.

[7] TESC URL: https://github.com/skbaek/tesc

Improve this answer
$\endgroup$
3
  • $\begingroup$ Why is it that "ATPs are mostly dealing with first-order logic"? $\endgroup$
    – Daniel Donnelly
    Commented Oct 31, 2022 at 15:05
  • 1
    $\begingroup$ Welcome to PA, Anja! $\endgroup$
    – Andrej Bauer
    Commented Nov 1, 2022 at 20:13
  • 1
    $\begingroup$ ATPs are mostly using first-order logic because the methods that are currently available are only suitable if there is no type system, or it is very simple. Usually the automation is based on refutation: the conjecture is negated and unsatisfiability is derived by one of the methods, like superposition calculus, tableaux method, unit propagation etc. The soundness (and completeness) of these methods is not ensured for dependent types that are used in type theories. There is some automation developed within PAs (like auto in Coq), but the performance does not yet scale compared to other ATPs. $\endgroup$
    – Anja Petković Komel
    Commented Nov 2, 2022 at 9:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.