Logic

What is a logic?

A study of correct inference.
Correct inference typically implies that it is truth preserving.
IOW, logic is the study of truth preserving inferences. For example:

• Truth preserving inference:

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.

• Non-Truth preserving inference:

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.

The goal is to formalize the notion of a correct inference. This requires three things:
• The syntax of a formal language.

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.

• The semantics of the formal language.

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 proof theory .

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.

Validity, Soundness, & Completeness

A sentence s is a valid consequence of a set of sentences S if and only if for all interpretations whenever all sentences of S are true in an interpretation, then s is true in that interpretation as well. Sentences that are true in all interpretations are called valid as well.

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.

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.

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.

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:

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.

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!).

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
------------------------------------------------------------------------------

```

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.

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.

Last updated: June 5, 1995.
Deepak Kumar
Bryn Mawr College
dkumar@cc.brynmawr.edu