| English | All men are mortal | Socrates is a man | Socrates is mortal |
|---|---|---|---|
| ACE | For all X, if X is a member of Man, then X is mortal. | Socrates is a member of Man. | Socrates is mortal. |
| MathML display | |||
| MathML markup | |||
| KIF | (forall ?X (=> (member ?X Man) (mortal ?X)) | (member Socrates Man) | (mortal Socrates) |
Example: arithmetic
| English | Five is the sum of three plus two. |
|---|---|
| ACE | Five is identical with the sum of three and two. |
| MathML display | 5 = 3 + 2 |
| MathML markup | <mn>5</mn> <mo>=</mo> <mn>3</mn> <mo>+</mo> <mn>2</mn> |
| KIF | (= 5, (+ 3, 2)) |
Example: equational reasoning
Example: temporal reasoning
- '3 dimensional'
- '4 dimensional'
Arguments
- All voters are Democrats or Republicans:
(forall ?X (=> (V ?X) (or (D ?X) (R ?X))))- No liberal is a Republican:
(forall ?X (=> (L ?X) (not (R ?X))))- Therefore, all liberals who vote are Democrats:
(forall ?X (=> (and (L ?X) (V ?X)) (D ?X)))- Run the Voters Example
Theorem Proofs
Normal forms and canonicalization
| KIF | Negation normal form | Conjunctive normal form | Disjunctive normal form |
Terms and Identity
Mathematical Induction
Skolemization