KR Language Components
A logical formalism
- Syntax for wffs
- Vocabulary of logical symbols (e.g., AND, OR, NOT, =>, <=>)
- Interpretation semantics for the logical symbols
E.g., �(=> A B)� is true if and only if B is true or A is false.
An ontology
- Vocabulary of non-logical symbols
- Relations, functions, constants
- Definitions of non-primitive symbols
E.g., (<=> (Bachelor ?x) (AND (Man ?x) (Unmarried ?x)))
- Axioms restricting the interpretations of primitive symbols
E.g., (=> (Person ?x) (Gender (Mother ?x) Female))
A proof theory
- Specification of the reasoning steps that are logically sound
E.g., From �(=> S1 S2)� and �S1�, conclude �S2�