Brought to you by EarthWeb
IT Library Logo

Click Here!
Click Here!

Search the site:
 
EXPERT SEARCH -----
Programming Languages
Databases
Security
Web Services
Network Services
Middleware
Components
Operating Systems
User Interfaces
Groupware & Collaboration
Content Management
Productivity Applications
Hardware
Fun & Games

EarthWeb Direct EarthWeb Direct Fatbrain Auctions Support Source Answers

EarthWeb sites
Crossnodes
Datamation
Developer.com
DICE
EarthWeb.com
EarthWeb Direct
ERP Hub
Gamelan
GoCertify.com
HTMLGoodies
Intranet Journal
IT Knowledge
IT Library
JavaGoodies
JARS
JavaScripts.com
open source IT
RoadCoders
Y2K Info

Previous Table of Contents Next


3.1.1. Propositional Logic

Propositional logic was first proposed by the English mathematician George Boole to specify a way in which elementary sentences called propositions can be combined using connecting words like and, or, not, etc. Boole's logic was the first departure from the Aristotelian tradition, which considered syllogisms as the only valid forms of correct arguments. But the 19 syllogisms discovered by Aristotle describe only a small subset of correct arguments. For instance, we cannot connect together several sentences to form a hypothesis as we can in propositional logic, in which we can construct hypotheses and conclusions of arbitrary complexity. However, in propositional logic, we cannot analyze the structure of the proposition as we can in a syllogism. Thus, Boole's propositional logic and Aristotle's syllogisms describe two disjoint families of correct reasoning forms, but they do not exhaust all the correct forms.

To construct sentences, propositional logic uses an alphabet of logical symbols with a fixed meaning (connectives, parentheses), and a set of non-logical symbols with variable meaning (propositions), with which sentences (well-formed formulae) can be constructed. A truth assignment (or interpretation) assigns formulae one of the values, true or false. A formula that is valid under every interpretation is called valid. Valid formulae are called tautologies. Propositional logic is decidable and there are procedures for establishing the validity of a formula (e.g., truth tables). However, the problem of satisfiability for propositional logic is known to be NP-complete. Finding a model that satisfies a formula is known as the SAT problem (Gallier).

3.1.2. First-Order Logic

First-order logic (FOL), which was first formalized by the German mathematician Gottlob Frege in 1879, has played an important role in the development of mathematics, computer science, and artificial intelligence. FOL extends the correct forms of reasoning of syllogisms and propositional logic by defining a more general ontological view of the world in which the building blocks are objects and relations (predicates) among objects. First-order logic was introduced to AI by John McCarthy in 1958 (McCarthy). First-order logic assumes that the world consists of objects with their own properties that distinguish them from other objects, and relationships among the objects. Some of these relationships are functions that identify objects and some are relations that characterize a subset of objects. The domain can be any set. Universal and existential quantification is used to define relations over elements of potentially infinite domains. A term denotes an element of the domain; predicates can take one of the values true or false. First-order logic is more expressive than propositional logic and we can express facts about the world that cannot be expressed with propositional logic. Proof procedures for first-order logic have been developed that are sound and complete, although when one introduces particular theories (e.g., lists, arithmetic), they may become incomplete. Proof procedures in general are semi-decidable, which means that if a formula is valid there are proof methods that will establish this fact, but if the formula is not valid, these same methods may run forever without detecting this fact. Two of these procedures are resolution and mathematical induction.

The resolution procedure was first proposed by Robinson (Robinson). It is a simple yet extremely powerful rule of inference that has been shown sound and complete, and the associated proof procedure is very amenable to machine implementation. Resolution stimulated research and development in automatic theorem proving and found many applications in natural language understanding, planning, database systems, and logic programming, among other areas.

Resolution is a refutation system, that is, to prove that a formula [capital phi] follows from a set of formulae [open triangle], we negate [capital phi], add the negation of [capital phi] to [open triangle], and try to derive a contradiction. Resolution requires [capital phi] and the formulae in [open triangle] to be in a normal form called clausal form, in which each formula is expressed as a disjunction of literals. A procedure exists to convert any set of formulae into clausal form. Resolution also requires a unification procedure that collapses two predicates P(t1, ..., tn) and into a predicate by finding a most general unifier [gamma], which is obtained by performing substitutions among the terms ti and to yield that is:

The resolution rule is given as follows: Suppose that [alpha] and [beta] are two clauses, if there is a literal [omega] in [alpha] and a literal [omega] in [beta] such that [capital phi] and [omega] have a most general unifier [gamma], then we can infer the clause obtained by applying the substitution [gamma] to the union of [alpha] and [beta] minus the complementary literals [capital phi] and [omega]:

Looking for a contradiction requires search. Many search techniques as well as constraints on the form of the clauses have been proposed to make the search efficient, such as linear resolution, ordered resolution, SL resolution, and SLD resolution, which, with a depth-first search strategy, is used in the PROLOG programming language as well as in numerous expert system shells.

Mathematical induction is a family of inference rules that is required for reasoning about object and events containing repetition. Since repetition is ubiquitous in many application areas and inductive reasoning is very difficult to automate, research has focused on the automation of proof for mathematical induction. Inductive proofs are characterized by the application of inference rules for mathematical induction such as Peano induction and structural induction on lists and other data structures. All these forms of induction are subsumed by a single, general schema of well-founded induction:

where is some well-founded relation of the type [tau], i.e., there is no infinite descending sequence: a1 a2 a3 ... . The data structure, control flow, time step, etc., over which induction is to be applied, is represented by the type [tau]. The inductive proof is formalized in a many-sorted or typed logical system. Success in proving a conjecture, P, by well-founded induction is highly dependent on the choice of x, [tau], and . For many types, [tau], there is an infinite variety of possible well-orderings, . Thus, choosing an appropriate induction rule to prove a conjecture is one of the most challenging search problems to be solved in automating mathematical induction.

Resolution and mathematical induction are being used in the design of many types of intelligent systems applications, which include natural language interfaces, verification and synthesis of programs and circuits, and programming languages.


Previous Table of Contents Next

footer nav
Use of this site is subject certain Terms & Conditions.
Copyright (c) 1996-1999 EarthWeb, Inc.. All rights reserved. Reproduction in whole or in part in any form or medium without express written permission of EarthWeb is prohibited. Please read our privacy policy for details.