I. Norvig Chapters 9 and 10: Inference in First-Order Logic

II. Chapter 9: Inference in First-Order Logic

A. Inference Rules Involving Quantifiers

1. Universal Elimination
2. Existential Elimination
3. Existential Introduction
4. Ways of giving names to quantified variables

B. Generalized Modus Ponens

1. Allows substitution of multiple variables in an expression.
2. Efficient

a) Takes bigger steps, combining several small inferences into one.
b) Takes steps that are guaranteed to help.
c) Uses a precompilation step that converts sentences into canonical form.

3. Canonical Form
4. Horn Sentences
5. Unification: takes two atomic sentences p and q, then returns a substitution that makes p and q the same.
6. Standardize Apart: renaming variables in different sentences to avoid name clashes.
7. Most General Unifier: The substitution that makes the least commitment about the bindings of the variables.

C. Forward and Backward Chaining

1. Forward Chaining

a) Start with the sentences in the KB and generate new conclusions that can allow more inferences to be made.
b) Triggered by the addition of a new fat to the KB
c) Data-Directed / Data-Driven: Inference processes are not directed toward solving any particular problem.

2. Backward Chaining

a) Start with something that we wish to prove, find implication sentences that conclude it, then attempt to establish their premises.
b) Designed to find all answers to a question.
c) Functionality for Ask procedure.

3. Questions

a) Under what conditions is forward chaining preferred over backward chaining?
b) What are the costs and benefits of forward and backward chaining?

D. Completeness

1. Modus Ponens is incomplete: There are sentences entailed by the KB that the procedure cannot infer.
2. Benefits of a complete proof procedure for mathematical statements

a) All conjectures can be established mechanically.
b) Mathematics can be established as the logical consequence of a set of logical axioms.
c) A complete proof procedure for FOL would allow a machine to solve any problem that can be stated in FOL.

3. Godel's completeness theorem: Showed that in FOL, any sentence that is entailed by another set of sentences can be proved from that set. We can find inference rules that allow a complete proof procedure.
4. Entailment in FOL is semidecidable; we can show that sentences follow from premises, but cannot always show that they do not.

E. Resolution: A Complete Inference Procedure

1. Derives atomic conclusions.
2. Conjunctive normal form: Conjunction of disjunctive clauses.
3. Implicative* normal form: An implication with a conjunction of atoms on the left and a disjunction of atoms on the right.
4. Resolution is a generalization of modus ponens.
5. Refutation: Proof by contradiction
6. Conversion to Normal Form

a) Eliminate implications
b) Move negation inwards
c) Standardize variables
d) Move quantifiers left
e) Skolemization: the process of removing existential quantifiers by elimination.
f) Distribute conjunction over disjunction.
g) Flatten nested conjunctions and disjunctions.
h) Convert disjunctions to implications.

7. Equality

a) Unification only does a syntactic test based on the appearance of the argument terms, not a true semantic test based on the objects they represent.
b) Can axiomize equality: reflexive, symmetric, and transitive
c) Demodulation

8. Resolution strategies

a) Unit preference / unit clause: Do resolutions where one of the sentences is a single literal.
b) Set of support: Starts with a subset of sentences called the set of support.. Generates goal-directed proof trees.
c) Input resolution: Every resolution combines one of the input sentences with some other sentence. Complete for KBs that are in Horn form, but incomplete in the general case.
d) Linear resolution: Generalization of Input resolution. Complete.
e) Subsumption: Eliminates all sentences that are subsumed by (i.e., more specific than) an existing sentences in the KB.

9. Completeness of Resolution

a) Resolution is refutation-complete: If a set of sentences is unsatisfiable, then resolution will derive a contradiction.
b) See proof.

F. Questions

1. Why doesn't unit preference reduce the branching factor enough to enable us to solve medium-sized problems?
2. What are the benefits of inference rules?

III. Chapter 10: Logical Reasoning Systems

A. Types of automated reasoning systems

1. Theorem provers and logic programming languages: use resolution to prove sentences in FOL.
2. Production systems: Use implications as their primary representation. The consequent of each implication is an action recommendation.
3. Frame systems and semantic networks: Taxonomy of objects and relations between them.
4. Description logic systems: Designed to express and reason with complex definitions of, and relationships between, objects and classes.

B. Tasks that the system must perform

1. Add a new fact to the KB.
2. Derive some facts implied by the conjunction of the knowledge base and a new fact (forward chaining).
3. Decide if a query is entailed by the KB.
4. Decide if a query is stored in the KB.
5. Remove a sentence from the KB.

C. Indexing, Retrieval, and Unification.

1. Fetch: finds sentences in the KB that unify with the query.
2. Table-based indexing.
3. Tree-based indexing.

D. Logic Programming Systems

1. Logic programming views the program and inputs as logical statements about the world, and the process of making consequences explicit as a process of inference.
2. Prolog: negation as failure.

a) Inference done by backward chaining, DFS.
b) First-to-last, left-to-right evaluation order
c) No occur-check in unification.

3. Constraint Logic Programming: extends the notions of variables and unification to allow the addition of constraints.
4. Metareasoning: Reasoning about reasoning.
5. Backjumping.
6. Dependency-directed backtracking.

E. Theorem Provers

1. Theorem provers separate control information from the KB.
2. Components

a) set of support
b) usable axioms
c) rewrites and demodulators
d) control strategy

3. Proof checker
4. Socratic reasoner: Ask function is incomplete; however, the system can always arrive at a solution if asked the right series of questions.

F. Forward-Chaining Production Systems

1. Components of a production system

a) working memory
b) rule memory
c) Each cycle includes a match phase, where the system computes the subset of rules whose left-hand side is satisfied by the current contents of the working memory.
d) Conflict resolution phase.
e) Act phase.

2. Example systems

a) ACT
b) SOAR

G. Frame Systems and Semantic Networks

1. Whether the language uses strings or nodes and links, and whether it is called a semantic network or a logic, has no effect on its meaning or on its implementation. - p317
2. Semantic networks and frame systems could be implemented in logic, i.e., FOL.
3. Benefits of Frame systems and Semantic networks

a) Easy to visualize the inferencing steps.

4. Simple query language.
5. Inheritance
6. Reification: Where relations are treated as objects, not as predicates.
7. Multiple inheritance.
8. Note: inheritance with exceptions is nonmonotonic.
9. Nonmonotonic logic.
10. Benefits of reduces expressiveness.

a) Easy to understand inheritance.
b) Capture inheritance information in a modular way.
c) efficiency

H. Description logics

1. Focus on categories and their definitions
2. Subsumption: Is one category a subset of another?
3. Classification
4. Usually lack negation and disjunction.

I. Managing Retractions, Assumptions, and Explanations

1. Want to be able to retract a sentence without causing inconsistencies.
2. Truth Maintenance Systems

a) Justification-based TMS
b) Assumption-based TMS

3. Computational complexity of truth maintenance is NP-hard.

J. Other concerns

1. Trade-off between expressiveness of the system and efficiency.
2. Clear semantics for the representation language enhances usability.
3. Simplifying the executing model aids understanding of the inferencing steps.

K. Questions

1. What is the difference between Fetch and Ask? How are they related?
2. What determines the cost of inference?
3. Under what conditions should table-based inferencing be employed?
4. Give a specific example of a problem that requires metareasoning? Is there such a problem, if so, why?

L.