If there is a potato in the tailpipe, the car will not start.
There is a potato in the tailpipe.
Therefore, the car will not start.
If there is a potato in the tailpipe, the car will not start.
My car will not start.
Therefore, there is a potato in the tailpipe.
Inference is a relationship between sentences. Thus in order to formalize the notion of a correct inference, one first needs to define what constitutes well-formed sentences.
A specification of the meanings of the well-formed sentences of the formal language. I.e., under what conditions is a sentence true.
Meaning is defined in terms of some interpretation. The meaning of a sentence in an interpretation is the truth value of the sentence.
A formal specification of what constitutes correct inference. A proof theory consists of axioms, and a set of inference rules. While this is a purely syntactic formalization, it is closely related to the semantics of the formal language. It is the abstract specification of an inference engine that will compute valid consequences (see below) of a set of sentences.
A proof theory is said to be sound when every sentence s that can be derived from a set of sentences S is also a valid consequence of S.
A proof theory is said to be complete when every sentence s that is a valid consequence of a set of sentences S can also be formally derived.
Consider the following:
Tweety is a bird.
Birds fly.
Therefore, Tweety flies.
What if we also know that:
Penguins are birds.
Penguins do not fly.
Tweety is a penguin.
Therefore, Tweety does not fly!
Default reasoning provides a solution. A default rule specifies a plausible inference:
Typically birds fly.
I.e., In the absence of evidence to the contrary, all birds fly. Since it can now be shown that Tweety is a penguin, and penguins do not fly, and hence Tweety does not fly, the default rule will not be applicable.
In the absence of the fact that Tweety is a penguin, the default inference would still be possible. Later on, if it is asserted that Tweety is a penguin, the earlier inference would have to be retracted. Such logics are called nonmonotonic. One has to extend FOPC to include such default rules.
A bird flies if it is not abnormal.
Circumscription then allows the inference engine to assume that only the things that can be shown to be abnormal are in fact all the things that are abnormal. Hence, in the above rule, one does not have to show that a bird is not abnormal in order to prove that it flies. The above rule can also be written as
If something is a bird and it does not fly, then it is abnormal.
In the example above, when it is known that Tweety is a penguin, it will lead the system to conclude that Tweety is abnormal, and hence prevent the inference that Tweety flies.
Both assumption-based as well as justification-based TMS systems may be presented. It may also be possible to use the code that comes with Forbus & de Kleer's book.
Ginsberg's text also starts with the basic concepts, presents FOPC, an extensive treatment of resolution, and unification. Several resolution strategies are also presented. There are also short surveys of assumption-based TMS and nonmonotonic reasoning.
The coverage of topics in Russell & Norvig is also pretty close to what is presented above. However, instead of nonmonotonic logics, there is an extended discussion of resolution (in addition to modus ponens), and details of PROLOG design and implementation. The examples are all embedded in the agent-oriented approach ("agents that reason logically").
Tanimoto's chapter on logical reasoning presents propositional calculus, followed by predicate calculus and resolution, unification, completeness proof for resolution, resolution strategies, and PROLOG. There is a small section on nonmonotonic reasoning that presents circumscription.
Rich & Knight present predicate calculus, resolution, and unification. There is a small section on natural deduction. A separate chapter presents nonmonotonic methods: default logic, circumscription, and truth maintenance.
Luger & Stubblefield's presentation begins with propositional calculus, followed by predicate calculus (syntax and semantics), inference rules, and unification. later in the text, there is a whole chapter devoted to resolution.
Below is a table showing a survey of six AI texts and their coverage of logic. Pairs of numbers indicate the approximate number of pages of text, and an estimate of the number of lectures that will typically be required to cover all the material in the text. Each lecture is assumed to be 75 minutes long. A typical semester has about 13 weeks of lectures, each week having two 75 minute lectures, giving a total of 26 lectures.
------------------------------------------------------------------------------ Dean, Allen &, Russell & Rich & Luger & Aloimonos Ginsberg Norvig Tanimoto Knight Stubblefield ------------------------------------------------------------------------------ Overall Text 500/40 400/24 850/52 760/42 580/40 700/40 ------------------------------------------------------------------------------ Logic 100/12 122/7 180/9 60/5 70/5 60/3 ------------------------------------------------------------------------------
Please write back to the author for any corrections/additions
Forbus & de Kleer : Building Problem Solvers, MIT Press, 1994.
Genesereth & Nilsson : Logical Foundations of Artificial Intelligence , Morgan Kaufmann Publishers, Los Altos, CA, 1987.
Ginsberg : Essentials of Artificial Intelligence, Morgan Kaufmann Publishers, 1993.
Artificial Intelligence: Structures and Strategies for Complex problem Solving, Second Edition, Benjamin Cummings Publishing Company, 1993.
Reichgelt : Knowledge Representation: An AI Perspective, Ablex Publishing, 1991. (A small, but comprehensive text on classic KR techniques. The text summarizes most of the important discussions from papers in the Brachman & Levesque collection. Lots of stuff in this page comes from its chapter on logic.)
Rich & Knight : Artificial Intelligence, Second Edition, McGraw Hill, 1991.
Russell & Norvig : Artificial Intelligence: A Modern Approach, Prentice Hall, 1995.
Shapiro : The Encyclopedia of Artificial Intelligence, Second Edition, John Wiley & Sons, Inc., 1992.
Tanimoto : The Elements of Artificial Intelligence Using Common Lisp, Second Edition, Computer Science press, 1995.