Formulas and proof syntax

Logical connectives
. conjunction
+ disjunction
=> implication
<=> equivalence
- negation
F false
Operator priority : (high) - & + => <=> (low)
Between two identical operations, the left operation is prioritary, except for implication

A . B . C est (A . B). C
A + B + C est (A + B) + C
A => B => C est A => (B => C)
A . B + C est (A . B) + C
A . B => C + D est (A . B) => (C + D)
- A + B est (- A) + B
A proof starting with the line case c followed by the assumption e : A and terminated by the corresponding end case c
is a proof of e : - A.
The proofs are S4-tableaux-proof of the formula given, so contain formulas of logic S4
with the operations [] (necessary) and <> (possible).

examples | rules | syntax | info | home| download| basis of the method (in french) Last Modified : 17-Dec-2021