Propositional Logic

⟨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':

Wff:

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.