Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or a tree proof (a.k.a. semantic tableau).

**The Tree Proof Generator by Wolfgang Schwarz**

This section is devoted to provers or verifiers of theorems in mathematical logic.

**The Tree Proof Generator by Wolfgang Schwarz**Enter a formula of standard propositional, predicate, or modal logic. The page will try to find either a countermodel or a tree proof (a.k.a. semantic tableau).

**Proof in first order logic by resolution**Given a list of clauses, as well as limits on the time of proof and the size of the clauses, the software tries to build a proof of the empty clause within the imposed limits.

**Svejdar proof method for GL logic****G4 Prover**This prover is a fork that I developed from seqprover.pl that is Naoyuki Tamura’s prover for sequent calculus CL-X. I am a lot indebted to Naoyuki Tamura’s work, because I needed to change almost only the logical rules of his program to succeed in writing this prover that provides proof in (...)

**A Linear Logic Prover**This small program searches a cut-free proof of the given two-sided sequent of first-order linear logic. Of course, the proof search of linear logic is undecidable. Therefore, this program limits the number of contraction rules for each path of the proof at most three (this threshold value can (...)

- 0
- 5