A knowledge base (KB) is a KR&R-based system, that is defined as a collection of sentences that represents what the agent/program believes about the world. Sentences in the KB are explicit knowledge of the agent. Logical consequences of the KB are implicit knowledge of the agent.
Proof procedures
To compute the implicit knowledge of the KB, we need an algorithm that allows us to reason with our knowledge. In other words, we need to represent the knowledge as logical formulas, and apply the procedure for generating logical consequences.
Mechanical proof procedures work by manipulating formulas. They do not know or care anything about interpretations, but still respect the semantics of interpretations.
i.e., they don’t know the English description that we understand. They only know what is given to them as a structure/sentence.
A proof procedure is sound if whenever it produces a sentence by manipulating sentences in a KB, then is a logical consequence of KB, i.e., .
i.e., all conclusions arrived at via the proof procedure are correct, they are logical consequences.
A proof procedure is complete if it can produce all logical consequences of the KB.
If , then the procedure can produce .
Resolution is both sound and complete for propositional and first-order logic.