- 〈Wff〉 ::= 〈Wff〉 -> 〈Disjunction〉
| 〈Disjunction〉
- 〈Disjunction〉 ::= 〈Disjunction〉
or 〈Conjunction〉
| 〈Conjunction〉
- 〈Conjunction〉 ::= 〈Conjunction〉
and 〈Literal〉
| 〈Literal〉
- 〈Literal〉 ::= not 〈Literal〉
| 〈Variable〉
| ( 〈Wff〉 )
- NB. often allow & for "and", etc.
- -- Syntax of Well Formed Formulae (Wff) --
Type a Wff in the area, press 'go':
- CNF: conjunctive normal form.
- DNF: disjunctiove normal form.
- tautology: always true for all cases of variables being true/false.
- contradiction: never true for any cases of variables being true/false.
- satisfiable: sometimes true for some cases of variables being true/false.