Table of logic symbols

http://en.wikipedia.org/wiki/Table_of_logic_symbols

implies; if .. then
⇒

→

⊃

http://en.wikipedia.org/wiki/First-order_logic


Every propositional wff α can be converted into a formula α′ in
Conjunctive Normal Form (CNF) in such a way that |= α ≡ α′.
1. eliminate ⊃ and ≡ using (α ⊃ β) -> (¬α ∨ β) etc.
2. push ¬ inward using ¬(α ∧ β) -> (¬α ∨ ¬β) etc.
3. distribute ∨ over ∧ using ((α ∧ β) ∨ γ) -> ((α ∨ γ) ∧ (β ∨ γ))
4. collect terms using (α ∨ α) -> α etc.


http://en.wikipedia.org/wiki/Conjunctive_normal_form

http://www.enm.bris.ac.uk/ai/enjl/

http://www.enm.bris.ac.uk/ai/enjl/logic1.pdf
• 1. The connectives → and ↔ are eliminated using the equivalences
A ↔ B ≡ ( A → B) ∧ (B → A) and then A → B ≡ (¬ A∨ B)
• 2. Secondly, De Morgan’s Laws are applied as widely as possible
¬( A∧ B) is replaced by (¬ A∨ ¬ B)
¬( A∨ B) is replaced by (¬ A∧ ¬ B)
• 3. Multiple negations are reduced using DNEG e.g. ¬¬ A is replaced by A
• 4. The DISTOR rule is frequently applied

After the above procedures have been applied the original sentence is in conjunctive
normal form. Further simplifications can then be made by applying rule 1 (section 4) to
eliminate tautologies e.g. ((¬ A∨ A) ∧ B) ≡ B and repetitions within a clause can be
suppressed using IDOR e.g. A∨ A∨ A ≡ A. Also, if, in a normal form, a clause Ci is
included in another clause C j , the COR and AOR mean that the clausal brackets can be
removed e.g. (( A∨ B) ∨ D) ≡ ( A∨ B∨ D) ≡ ( A∨ ( B∨ D)) etc. Finally rule 1 can be used to
reduce a normal form containing a logically false clause to a logically false clause. Forms
simplified by the above procedures are said to be pure normal forms.

6. ≡ ((P ∧ ¬R) ∧ Q) ∨ (( ¬P ∨ R) ∨ ¬S)
7. ≡ (¬ ( ¬P ∨R ) ∧ Q ) ∨ ( (¬P ∨ R ) ∨ ¬S)8. ≡ ((¬( ¬P ∨ R ) ∧ Q ) ∨ (¬P ∨ R )) ∨ ¬S
9. ((¬ (¬P ∨ R ) ∧ Q) ∨ ( ¬P ∨ R)) ≡ ( Q ∨ ( ¬P ∨R ))
10. ((¬ (¬P ∨ R ) ∧ Q) ∨ ( ¬P ∨ R)) ∨ ¬S ≡ Q ∨¬P ∨ R ∨ ¬S

Skolemization
∃x∀yR(x,y) |= ∀y∃xR(x,y)
∀y∃xR(x,y) |≠ ∃x∀yR(x,y)

∃x∀y∃zP(x,y,z) to ∀yP(a,y,f(y))

Abbreviations:
(α ⊃ β) for (¬α ∨ β)
safer to read as disjunction than as “if ... then ...”
(α ≡ β) for ((α⊃β) ∧ (β⊃α))