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

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.

• 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. Commented Feb 9, 2022 at 2:43
• Of interest: Logical calculation with tableaux Commented Mar 3, 2022 at 14:20

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.

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.

• I actually knew nothing about HOL Light (besides the fact that it exists) before today. Thanks for the reference to the book. Commented Feb 8, 2022 at 21:39

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

• I think it's the same thing as a connection tableau. You make a tree and try to get a contradiction in every branch of the tree. In the propositional logic case, the tableau calculus is decidable but not very efficient. I was assuming that a proof assistant based on tableau calculi would either let the user manually instantiate free variables, or manually unify terms, or manually specify a heuristic in some way to try to guide the proof assistant to a closed tableau. Using AI for this is interesting. Do you know of any papers describing training an AI to make tableau proofs? Commented Feb 9, 2022 at 3:07
• Also, I'm pretty sure that without doing clever things, a tableau based proof assistant produces really repetitive proofs (if you split the wrong disjunction early on you effectively have to solve the same problem twice), and also doesn't make effective use of lemmas. I'm curious how existing proof assistants have solved these problems. Commented Feb 9, 2022 at 3:12
• As for references of AI + connection provers, I would Google for "Josef Urban connection prover". But here are some papers: Guiding Inferences in Connection Tableau by Recurrent Neural Networks, Machine Learning Guidance and Proof Certification for Connection Tableaux, Reinforcement Learning of Theorem Proving, Towards Finding Longer Proofs, ... Commented Feb 9, 2022 at 3:16
• MaLeCoP Machine Learning Connection Prover, FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. There are probably more... Commented Feb 9, 2022 at 3:17