Tableau

Propositional Classical Logic

Good old classical propositional logic. The decision problem is NP-complete.

When you enter a formula A, then "closed" means that A is a
theorem because the tableau for ~ A is closed, and "open" means
that it is not a theorem because the tableau for ~ A is open.

Results
Query

formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| ~ formula

Info
pc.ml : Download
pclib.ml : Download

Propositional Dynamic Logic PDL(UEV)

The rules of this prover and their proofs of soundness and completeness are given in a manuscript which can be found at http://arxiv.org/abs/0711.1016 via the world wide web. For an introduction to PDL see http://plato.stanford.edu/entries/logic-dynamic/ When you enter a formula A, then "closed" means that A is a theorem because the tableau for ~ A is closed, and "open" means that it is not a theorem because the tableau for ~ A is open.
Results
Query
'''Syntax'''
_ ::= blank

AFml ::= a | b | c | ...

APrg ::= p | q | r | ...

Prg π ::= APrg | π ; π | π U π | _?_φ | _* π

Fml φ ::= AFml | Verum | Falsum | ~_φ | φ  v φ | <π> φ | φ -> φ | < π > φ | [ π ] φ

''Notes:''

(1) Star (*) is a prefix operator rather than a postfix one so *a is okay but a* is not.

(2) Star (*) and test (?) require a space before them.

(3) Negation ~ requires a space after it so ~ ~ p0 is okay but ~~p0 is not okay.
Info
pdlMarkNoSnf.ml : Download
pdlMarkNoSnfFunctions.ml : Download
Syndicate content