[Solved]: Why do some inference engines need human assistance while others don't?

Problem Detail: 

^{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.}

Asked By : Guy Coder

Answered By : Raphael

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).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/879

 Ask a Question

 Download Related Notes/Documents