Formulas and proof syntax
Logical connectives
.
conjunction
+
disjunction
=>
implication
<=>
equivalence
-
negation
F
false
[]
necessary
<>
possibly
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
est
(
[]
A
)
=>
B
A
.
B
+
C
est
(
A
.
B
)
+
C
A
.
B
=>
C
+
D
est
(
A
.
B
)
=>
(
C
+
D
)
-
A
+
B
est
(
-
A
)
+
B
<>
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
examples
|
rules
|
syntax
|
info
|
home
Last Modified : 17-Jan-2010