16
$\begingroup$

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

A closed tableau makes the branching structure of a proof using case analysis very obvious.

I like tableau calculi for proving stuff by hand; especially validating simple statements in nonclassical propositional or modal logics. For this purpose, tableau calculi are quite convenient and tableau proofs are short.

For larger things though, especially when using FOL, proving something by hand using this method is tedious ... largely because of the need to Skolemize the formula and rewrite the matrix of wffs in negation normal form.

I'm curious whether there are any well-known proof assistants based on the method of analytic tableaux or are capable of exporting tableau proofs in some format.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ Is this the same as connection tableau? If so there are a number of light-weight automated theorem provers for FOL which use connection tableau. For example, leanCOP (unrelated to the Lean theorem prover) is one written in Prolog. Another, rlCOP, uses reinforcement learning to guide the search. There are others also with names like mlCOP. I'm not aware of them being used as interactive proof assistants (for humans), but connection tableaux is a good environment for interacting with an AI agent since it is a light-weight (and cut-free) logical system with a finite action space. $\endgroup$
    – Jason Rute
    Commented Feb 9, 2022 at 2:43
  • $\begingroup$ Of interest: Logical calculation with tableaux $\endgroup$
    – Guy Coder
    Commented Mar 3, 2022 at 14:20

2 Answers 2

Reset to default
10
$\begingroup$

I take it you already know the answer to this.

HOL Light was written by John Harrison (ref) who also authored "Handbook of Practical Logic and Automated Reasoning". (site) Think of the book as a very detailed introduction to the code for HOL Light. (GitHub)

The book takes one from Boolean Logic all the way up to Interactive theorem proving.

If you look at the provided OCaml code you will see tableaux.ml.

After rereading your question noticed this part.

I'm curious whether there are any well-known proof assistants based on the method of analytic tableaux or are capable of exporting tableau proofs in some format.

I don't know if it can export tableau proofs in some format, it has been a decade since I used that code. However I might be rewriting the code again into SWI-Prolog and if I do I will try to keep this in mind.

How do I know this book so well, I am Eric noted at the top of the page and on the errata page.

If you do use the code don't forget the fixed code noted at the end of the errata.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I actually knew nothing about HOL Light (besides the fact that it exists) before today. Thanks for the reference to the book. $\endgroup$
    – Greg Nisbet
    Commented Feb 8, 2022 at 21:39
4
$\begingroup$

(Turning my comment to an answer, but downvote if I've misunderstood.)

Is this the same as connection tableau? If so there are a number of light-weight automated theorem provers for FOL which use connection tableau. For example, leanCOP (unrelated to the Lean theorem prover which came later) is one written in Prolog. Another, rlCOP, uses reinforcement learning to guide the search. There are others also with names like mlCOP.

I'm not aware of them being used as interactive proof assistants (for humans), but connection tableaux is a good environment for interacting with an AI agent since it is a light-weight (and cut-free) logical system with a finite action space.

Also, since Mizar uses FOL, it can export to a format usable by connection provers. See the MPTP2 project and Mizar40. (I'm not sure how easy it is to translate from other theorem provers, but in some sense I think that is how Hammer's work, by first translating, say, Coq or Isabelle to some FOL statement which is processed by a FOL ATP.)

Improve this answer
$\endgroup$
4

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.