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.
What if we also know that:
Penguins are birds.
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.
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.
First-Order Predicate Calculus (FOPC)
In the context of the above concepts, introduce the syntax,
semantics, and a proof theory for FOPC ( resolution?).
One may wish to review the above concepts for a propositional logic,
prior to FOPC.
Building a logic-based inference engine
Present a detailed description of how proofs by resolution work.
This is also a good place to introduce unification. Coversion
of FOPC wffs to clause form, skolemization, resolution strategies,
Horn clauses, PROLOG, can be presented.
Decidability
A problem is said to be decidable if there exists a
computational process that solves the problem in a finite number of steps.
Typically, a proof theory for FOPC is only semidecidable. I.e.,
there is a computational process that after a finite time will answer
"yes" if s is a valid consequence of a set of sentences S, but
there is no process that will answer "no" if it is not. Some logics
can be made decidable by sacrificing some expressive power (and some
inference rules).
Default Reasoning
If time permits, default reasoning and/or circumscription can also be
introduced.
Birds fly.
Therefore, Tweety flies.
Penguins do not fly.
Tweety is a penguin.
Therefore, Tweety does not fly! Circumscription
Circumscription is a rule of inference that facilitates the
conclusion that the objects that can be shown to have some property are
infact allthe objects that have that property. The default rule
from the above example is stated as follows: Truth Maintenance Systems
The above topics provide a good lead into a discussion of truth maintenance
systems. Depending upon the time available the depth of coverage may vary.
Of course a TMS can also be independently motivated, by creating a KR system
that stores all its inferences. In the context of a changing knowledge base,
it is likely that addition/deletion of later facts can cause inconsistencies.
Logic in AI Texts
Dean, Allen, & Aloimonos: Their chapter on logic starts by introducing
propositional logic, and in that context, it presents most of the
fundamental concepts outlined above. That is followed by a similar treatment
of FOPC. The chapter also presents default rules, circumscription, and an
overview of TMS. The outline of the chapter is very close to the structure
of this page (and this page was written prior to a review of this text!).
------------------------------------------------------------------------------
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
------------------------------------------------------------------------------
References & Resources
Clicking below on names will take you to the individual's home page. Generally
a good starting point for locating current information. Clicking below on
titles of the publications will take you to homepages of the documents where
other resources like code, instructional materials, and related software
may be available.
Dean, Allen, & Aloimonos : Artificial Intelligence -Theory and
Practice, Benjamin Cummings Publishing Company, 1995.
Last updated: June 5, 1995.
Deepak Kumar
Bryn Mawr College
dkumar@cc.brynmawr.edu