5 Propositions and Inference

This chapter considers a simple form of a knowledge base that is told facts about what is true in the world. An agent can use such a knowledge base, together with its observations, to determine what else must be true in the world. When an agent is queried about what is true given a knowledge base, it can answer the query without enumerating the possible worlds, or even generating any possible worlds. This chapter presents a number of reasoning formalisms that use propositions. They differ in what is being proved, what background knowledge must be provided, and how the observations that the agent receives online are handled.

• 5.1 Propositions
  • 5.1.1 Syntax of Propositional Calculus
  • 5.1.2 Semantics of the Propositional Calculus
• 5.2 Propositional Definite Clauses
  • 5.2.1 Questions and Answers
  • 5.2.2 Proofs
• 5.3 Knowledge Representation Issues
  • 5.3.1 Background Knowledge and Observations
  • 5.3.2 Querying the User
  • 5.3.3 Knowledge-Level Explanation
  • 5.3.4 Knowledge-Level Debugging
• 5.4 Proving by Contradictions
  • 5.4.1 Horn Clauses
  • 5.4.2 Assumables and Conflicts
  • 5.4.3 Consistency-Based Diagnosis
  • 5.4.4 Reasoning with Assumptions and Horn Clauses
• 5.5 Complete Knowledge Assumption
  • 5.5.1 Non-monotonic Reasoning
  • 5.5.2 Proof Procedures for Complete Knowledge
• 5.6 Abduction
• 5.7 Causal Models
• 5.8 Review
• 5.9 References and Further Reading
• 5.10 Exercises