next up previous
Next: Foundations Up: Logic and Artificial Intelligence: Previous: The Logic-AI Marriage

A Taxonomy for Analyzing LAI

 

Modern first-order logic (denoted, hereafter, following tradition, by ` tex2html_wrap_inline773 tex2html_wrap_inline775 ') is the cornerstone of any respectable exposition of LAI; we give here a quick review of it in accordance with Glymour's Chapter 6 (``Symbolic Logic'') and Thayse's 1989, Chapter 1 (``Languages and Logic''):Thayse 1989 provides a more mathematically detailed account than Glymour, which isn't surprising: Glymour's intended audience is students in introductory philosophy courses. (Susan Russinoff (1995) claims that Glymour is too advanced for such introductory courses, because the students in question may have no background in logic, probability theory, or computability theory. We have found at Rensselaer, however, that Glymour is a remarkably effective text for Introduction to Philosophy.)

Given an alphabet (of variables tex2html_wrap_inline777 ; constants tex2html_wrap_inline779 ; n-ary relation symbols tex2html_wrap_inline783 ; functors tex2html_wrap_inline785 ; quantifiers tex2html_wrap_inline787 ; and the familiar truth-functional connectives ( tex2html_wrap_inline789 ), one uses standard formation rules (e.g., if tex2html_wrap_inline791 and tex2html_wrap_inline793 are well-formed formulas (wffs), then tex2html_wrap_inline795 is a wff as well) to build ``atomic'' formulas and then more complicated ``molecular'' formulas. >From sets of these formulas (say tex2html_wrap_inline797 ), given certain rules of inference (e.g., modus ponens: from tex2html_wrap_inline791 and tex2html_wrap_inline801 , infer tex2html_wrap_inline793 ), individual formulas (say tex2html_wrap_inline791 ) can be inferred; such a situation is expressed by meta-expressions like tex2html_wrap_inline807 . First-order logic includes a semantic side that systematically provides meaning for formulas involved. In first-order logic, formulas are said to be true (or false) on an interpretation, often written as tex2html_wrap_inline809 tex2html_wrap_inline811 . (This is often read, `` tex2html_wrap_inline809 satisfies tex2html_wrap_inline791 '', or `` tex2html_wrap_inline809 models (or is a model of) tex2html_wrap_inline791 ''.) For example, the formula tex2html_wrap_inline821 might mean, on the standard interpretation tex2html_wrap_inline823 for arithmetic, that for every natural number n, there is a natural number m such that m > n. In this case, the domain of tex2html_wrap_inline823 is N, the natural numbers, and G is the binary relation tex2html_wrap_inline835 ; i.e., > is a set of ordered pairs (i, j), where tex2html_wrap_inline841 and i is greater than j. Some formulas of tex2html_wrap_inline773 tex2html_wrap_inline775 are valid, in the sense that they are true on all interpretations. For example, any formula tex2html_wrap_inline851 of the form tex2html_wrap_inline853 is valid; such a fact is customarily written tex2html_wrap_inline855 . A formula that is true on at least one interpretation is satisfiable.

It is easy enough to generalize from this account to the broader concept of a logical system, and doing so is crucial for understanding LAI and the six books under consideration.Because, in the context of explicating LAI (and, for that matter, CAI), it's necessary to include syntactic, semantic, and proof-theoretic elements, our account of logical system is somewhat broader than the standard account that figures in (say) Lindström's Theorems. For the narrower account, as well as a nice presentation of these theorems, see Ebbinghaus et al. 1984. It's perhaps worth pointing out that semiotic systems may be justifiably regarded to be generalizations of logical systems. For a brief introduction to semiotic systems in the context of AI, see Fetzer 1994. A logical system includes an alphabet (the symbols from which well-formed formulas are to be built); a grammar specifying how wffs are to be generated; a semantic relation, a binary relation (e.g., tex2html_wrap_inline857 as presented in the previous paragraph) holding between interpretations (or other structures designed to formally model aspects of ``reality'') and formulas; and a proof theory that makes precise how reasoning in the system is to proceed.

It is also usually important that a logical system have associated with it a metatheory, which would address questions such as whether the system in question is sound, complete, decidable, and so on. Such metaproperties are determined by bringing mathematical tools to bear on the system in question.

To anchor things a bit, consider first a system even simpler than first-order logic, viz., the propositional calculus, tex2html_wrap_inline773 tex2html_wrap_inline861 , a familiar and simple logical system, and one introduced in solid fashion in Thayse 1989.This is as good a place as any to point out that there is in fact a volume, Thayse 1989a, that precedes Thayse 1989, with nice coverage of most of elementary logic and logic programming. Thayse 1989a isn't reviewed herein. tex2html_wrap_inline773 tex2html_wrap_inline861 has for an alphabet propositional variables tex2html_wrap_inline867 , and the truth-functional connectives; its grammar is the grammar of tex2html_wrap_inline773 tex2html_wrap_inline775 without rules covering the quantifiers; its semantics are based on truth-tables (so that, e.g., tex2html_wrap_inline873 holds iff tex2html_wrap_inline791 is true on every truth-value assignment in an exhaustive truth-table for tex2html_wrap_inline791 ); and the proof-theory of tex2html_wrap_inline773 tex2html_wrap_inline861 can be given by familiar natural-deduction rules (e.g., modus ponens). Another logical system, this one ``beyond'' tex2html_wrap_inline773 tex2html_wrap_inline775 , is second-order logic, tex2html_wrap_inline773 tex2html_wrap_inline889 , which adds relation variables tex2html_wrap_inline891 , to the alphabet of tex2html_wrap_inline773 tex2html_wrap_inline775 , which in turn allows (via the associated grammar) for formulas expressing such things as Leibniz's Law (two things are identical iff they have precisely the same properties):

displaymath897

Of course, logical systems are mathematical creatures. How does LAI end up with working programs? Suppose that we want to implement a logical system able to play the role of a guidance counselor in advising a high school student about which colleges to apply to. And suppose that we want to essentially work in tex2html_wrap_inline773 tex2html_wrap_inline775 . The first thing we need to do is create an ontology of the domain in question; accordingly, we may posit categories that include SATs, small liberal-arts colleges, national universities, grade-point averages, etc. All of these things must be representable by symbols from, and strings over, an alphabet of our devising (though part of the alphabet is unalterable; e.g., we know that we have the quantifiers). To focus the situation, suppose that we want a rule in such a system that says ``If a student has low SATs and a low GPA, then none of the top twenty-five national universities ought to be applied to by this student.'' Assume that we have the following interpreted predicates: Sx iff x is a student, tex2html_wrap_inline907 for x has low SATs, tex2html_wrap_inline911 for x has a low GPA, Tx for x is a top-twenty-five national university, and Axy for x ought to apply to y. Then the rule in question, in first-order logic, becomes

equation65

Let's suppose, in addition, that Steve is a student denoted by the constant s in the system and that he, alas, has low SATs and a low GPA. Assume also that v is a constant denoting Vanderbilt University (which happens to be a top twenty-five national university according the U. S. News & World Report's annual rankings). These facts are represented in the system by

equation68

and

equation70

Our implemented logical system, based as it is on first-order logic, can verify

displaymath929

that is, it can deduce that Steve ought not to apply to Vanderbilt.

At this point, we have identified, with respect to LAI, the following four fundamental categories: historical, philosophical, and mathematical foundations; creation and specification of logical systems themselves; metatheory; and ways of getting to an implementation. Given these categories, our books fall out as indicated in Table 1, where we have a range from 0 for ``no coverage'' to 1 for ``much coverage''.

  table72
Table 1: Breakdown of Coverage under Four Fundamental Categories

The remainder of the paper consists of selected discussion, via our six books, of these four categories, and then one final, brief section centered around a thought-experiment designed to display one of LAI's matchless virtues.


next up previous
Next: Foundations Up: Logic and Artificial Intelligence: Previous: The Logic-AI Marriage

Selmer Bringsjord
Mon Nov 17 14:57:06 EST 1997