Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here.

Why is it that automated theorem provers, i.e. ACL2, and SMT solvers do not need human assistance while proof assistants, i.e. Isabelle and Coq, do?

Find the series' next question here.

2 Answers

Validity of higher order formulae is in general not decidable and search spaces are huge, so all you can hope to do is to try to find a proof -- assuming it exists -- by cleverly enumerating the proof space (think sledgehammer, aptly named) but that is rough. Humans can play the oracle, providing the key lemmata to guide proof.

Automated provers, on the other hand, typically deal only with decidable (subsets of) logics, for instance propositional logic or subclasses of first-order logic, so they may run a long time but you know they are going to be successful eventually.

Note that there are approaches to enable proof assisstants to find those important lemmata, e.g. IsaPlanner. The tool guesses (inductive) lemmata by enumeration and random testing and then tries to prove them. By iterating the process, many lemmata of e.g. typical data type definitions can be found automatically.

Small ABC

• validity -- a formula is valid it holds whatever you assign to the free variables.
• free variables -- those variables that are not bound by quantifiers such as $\forall$ and $\exists$
• decidability -- a (boolean) property is (Turing) decidable if there is an algorithm that answers "yes" or "no" (correctly) after a finite amount of time.
• propositional logic -- also zero order logic; no quantification allowed.
• first order logic -- quantification is only allowed over individuals, i.e. you can do $\forall x. P(x)$ but not $\forall f. f(4) > 0$.
• higher order logic -- you may quantify over (and "build") arbitrarily complex objects, e.g. higher order functions (functions that take functions).
• @GuyCoder: I am not sure that is feasible, though. We can not write every answer such that it is digestible without prior knowledge. ATPs are advanced stuff; I would not recommend anybody learning them without a solid background in logics. Writing answers the way you seem to want them can only create an illusion of understanding but do not really help, imho. So everybody interested in your series should do some logics first, which we can also help with -- in other questions. – Raphael Mar 31 '12 at 7:34

I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio:

• On-board generic automated proof tools: old-school Isabelle tools like fast and blast (by L. Paulson) and newer automated provers like metis (by J. Hurd).

• External ATPs for First-Order Logic that are invoked via Sledgehammer: E prover, SPASS, Vampire. The proof that is found is analyzed to figure out which lemmas have contributed to it, reducing 10000s to 10s, and feeding the result to metis.

• External SMTs with partial proof reconstruction, notably for Z3 (by S. Boehme).

• Tools to find counter examples of unproven statements: Nitpick/Kodkodi (J. Blanchette) and Quickcheck (L. Bulwahn).

Does all that automated stuff make Isabelle an automated theorem prover?

Ultimately, I think the distinction of "ATP" vs. "ITP" is just some kind of "label" that tells how you want to position or "sell" your system: ATPs claim to be "push-button tools", but in practice you will have to interact (indirectly), by providing parameters or hints, or reformulating your problem. That might actually be quite challenging, due to the long runtimes that are common-place in the ATP community.

In contrast, an ITP system is made for people waiting on the spot, with half-decent access to internal proof states, to see what's missing to finish a proof. An ITP system that wraps up ATP tools in the manner of Isabelle might turn out more appealing for more users and more applications, than either ITP or ATP alone.

• It's been a while, but if I remember correctly neither fast nor blast are provers; they are basically heuristics using certain rules that may find a proof. (Of course, they are provers on a suitably small subset of formulae, which is true for any proof enumeration method.) – Raphael Mar 6 '13 at 6:53
• When you say "prover" do you actually mean "decision procedure" for a certain fixed language? Most ATP "provers" are semi-decision procedures, the way you characterized fast and blast. Note that blast was presented by L. Paulson as "A Generic Tableau Prover and its Integration with Isabelle" at some CADE workshop -- the paper appeared later in J. UCS 1999. Isabelle has more "provers" and that sense, e.g. metis, but also decision procedures for some special languages (subsets of arithmetic). – Makarius Mar 6 '13 at 10:00