P in Prop (propositions) F in Form (formulae)Syntax BNF
F ::= P | ~ F | F ==> FValue Domains
Bool = { true, false } boolean logic values rho in Assign = P --> Bool truth assignmentsSemantic Functions
MM : Form --> Assign --> Bool means MM mapps a formula and an assignment into a boolean value the assignment tells the truth values of atomic propositionsSemantic Equations
MM [P] rho = rho(P) MM [~F] rho = ~ MM [F] rho MM [F1 ==> F2] rho = ~ MM [F1] rho v MM [F2] rho