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”.