4
$\begingroup$

I am re-reading John Harrison's wonderful Handbook of Practical Logic and Automated Reasoning, and he has a rather idiosyncratic presentation of analytic tableaux.

What other tutorial implementations of analytic tableaux for first-order logic are there?

Improve this question
$\endgroup$
2
  • $\begingroup$ If anyone else is confounded with Harrison's transition in his book, it's because he appears to be implicitly relying on Prawitz's An improved proof procedure (1960), which would have been really nice to have known. $\endgroup$
    – Alex Nelson
    Commented May 9, 2022 at 18:51
  • $\begingroup$ (I mean, this is buried in the trail of citations; it's not really Harrison's fault. But it would have been nice to know to also look at that paper.) $\endgroup$
    – Alex Nelson
    Commented May 9, 2022 at 19:09

1 Answer 1

Reset to default
5
$\begingroup$

  • As far as I'm aware, leanTAP was written in just a few lines of Prolog, and it works with first-order formulas in Skolem normal forms. There's a tutorial implementation in OCaml which looks similar to it.

  • The Tree Proof Generator (GitHub) written in JavaScript works with general first-order formulas (though it seems to pre-process formulas into negation normal forms and then translates the proof back in the end?). It also implements equational reasoning (as described here) and modal logic, along with some heuristic optimizations.

  • This paper discusses the implementation of a tableau prover (blast tactic) for Isabelle. I am not sure how it translates tableau proofs (which are essentially a space-efficient representation of sequent calculus) into Isabelle proofs (natural deduction), but I've also found this discussion about such a translation in detail...

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Note that tableau "sequents" are one-sided, so the inferences performed in a tableau proof will map quite cleanly to natural deduction. (To show validity of an input formula, negate it and derive consequences using tableau rules until all branches are closed.) $\endgroup$
    – Michael Norrish
    Commented Apr 26, 2022 at 1:40
  • $\begingroup$ @MichaelNorrish Ah yes, I was probably thinking about "signed tableau" and reducing the number of DNE/RAA rules... $\endgroup$
    – Zhanrong Qiao
    Commented Apr 26, 2022 at 10:56

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.