Return to Answer

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

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

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.

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

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

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.

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

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.

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