Deductive Reasoning Systems Research Paper

(a) to predict states of the world not experienced before and to act accordingly; and

(b) to explain phenomena experienced in the world so that we can understand the reasons why they happened, and make them happen again if they are desirable, or otherwise avoid them in the future.

The combination of prediction and explanation is a fundamental and characteristic ingredient of the human way of life, which demonstrates the importance of reasoning.

Experience also shows that humans have a sense for the correctness of reasoning chains. In other words, we are not predicting arbitrary knowledge nor giving arbitrary explanations. Rather, there is an experienced correlation between the correctness of reasoning and its usefulness for predictions and explanations in the real world. On the other hand, humans are prone to mistakes in their reasoning. In coping with this and other weaknesses lies the motivation for the mechanization of reasoning in the form of reasoning systems.

This research paper describes the technical basis for reasoning systems, points out a number of issues of particular importance for the design of such systems, and briefly surveys their numerous applications.

1. Abstractions

In order to model the complex phenomena involved in reasoning various abstractions are needed, which are now discussed.

1.1 Formal Languages

Humans express their knowledge in natural language which, however, is too complex to be useful as a starting point for the mechanization of reasoning. A first important abstraction is therefore the representation of human knowledge in some formal language. It should be rich enough to be able to express all of our (propositional) knowledge, but simple enough to be useful for the manipulations needed in modeling reasoning, and concise enough to avoid ambiguities and redundancies. There are a number of formal languages meeting these criteria. They differ in the level of abstraction taken for the representation of knowledge, and in the comparative emphasis given to the various concepts involved.

The language of propositional logic takes the highest level of abstraction by formalizing knowledge at the level of entire propositions. The language of first-order logic is less abstract and much more expressive. It is probably the most popular formal language for knowledge representation, especially in the context of reasoning systems. Many knowledge representation formalisms (like the one used in Aristotelean syllogisms, semantic nets, description languages, etc.) are first-order formalisms in disguise, but lay the emphasis, for instance, on the concept of sets (as in the Aristotelean language) rather than on the functional (or Fregean) relationships among objects emphasized in first-order logic. Modal, transitional, and higher-order languages including the lambda calculus extend the expressiveness of first-order languages even further. For the purpose of this research paper, we restrict our discussion to the case of first-order logic. Most of our considerations generalize in some way to the other, more general, languages.

1.2 The Inferential Relationship

Reasoning takes place with a given body of knowledge, say K, already available. In the predictive mode of reasoning we want to determine what facts, say P, could be true in the future. Correct reasoning distinguishes between facts possible on the basis of K, and those which are impossible. In other words, there is a relation which associates K and P in the positive case. Following Frege, this relation is formally denoted by |=. That is, K|=P is short for expressing that P is a correct reasoning prediction on the basis of K. In the predictive mode of reasoning we thus want to determine P such that K|=P holds, or test for a given P whether it holds.

Human reasoning is mostly done in time, and to a significant extent also concerns knowledge about actions and changes taking place in time. On the other hand, a large part of the inferential relation is, so to speak, ‘timeless.’ To simplify further, most logical studies have abstracted from the issues concerning time and change. Only in the last few decades of the twentieth century did those issues become of great interest within Intellectics, the field covering both Artificial Intelligence and Cognitive Science. The result of those recent studies is that the timeless part of is already expressive enough to model also the part involving time, and thus the entire relation . Insofar this abstraction from time is without restriction of generality. Under this abstraction, the predictive mode of reasoning is called the deducti e mode of reasoning. Because of what was stated above, deductive reasoning at the surface is timeless reasoning, but may as well be regarded as predictive reasoning in general.

In the explanatory mode of reasoning based on K, we start with some observation O and basically look for some explanation E so that K, E |= O. This mode of reasoning is called abductive or inductive depending on the circumstances concerning O and E. Since is a relation, the difference with deductive reasoning is minor; instead of the second argument here just (part of ) the first one is to be determined. The relationship is even closer. In inductive reasoning we employ additional meta-knowledge, say M, which guides the process of generalizing from given observations. Taking this into account, inductive reasoning actually boils down exactly to deductive reasoning, namely in the form K, M, O |= E.

In summary, all prevailing modes of human reason-ing may actually be regarded as deductive reasoning. This explains why deductive reasoning systems have such a great importance for modeling inference in all its generality.

1.3 Syntactic Inference

The fundamental observation already made more than 2000 years ago by Aristotle and his predecessors is that reasoning (for the most part) is a matter of form rather than of content. This became apparent once knowledge was represented in a formalized way. The knowledge ‘apes are mammals’—in the sense of ‘whenever the property of being an ape holds then also the mammal property holds,’ or A→M, and ‘mammals have hair,’ M→H, allows us to conclude that ‘apes have hair,’ A→H. The inference is valid independently of the meaning of the words apes, mammals, and hair, or of the symbols A, M, H, for that matter. Rather, it is exclusively the form of the knowledge which sanctions the validity of such an inference. This fundamental property of reasoning enables machines, which are ignorant of the meaning of words or symbols, to perform correct inferences.

The example demonstrates a fundamental rule of inference: A→M and M→H implies A→H. It is called (a restricted form of ) resolution or (a slightly generalized form of ) modus ponens. As we see, it produces new knowledge by eliminating the inter-mediate atom M; the rule may also be seen as implementing a form of transitive closure.

In order to program computers to search for chains of inferences we first need rules of inference such as the one just discussed, in addition to the formal languages mentioned earlier. The combination of a formal language, along with a set of rules is called a (formal or logical) calculus. If F is some formula i.e., a propositional expression in the formal language under consideration, viz. first-order logic according to our convention, and G is a formula obtained from F by application of the rules of the calculus, then we write F|-G. Since is dependent on the calculus c—which, as in the case of formal languages, can be chosen from a great variety of alternatives—we should rather write |-_c, but omit the index whenever the calculus is clear from the context. We want to design calculi in such a way that F |- G holds if, and only if, (iff ) F |= G, in which case we speak of correct (if ) and complete (only if ) calculi. From now on we assume that the rules are chosen such that the resulting calculi are always correct and complete.

We go one step further in the abstraction process described in this entire section. According to the well-known deduction theorem, it holds that F|- G iff |-F→G. By applying this theorem iteratively we can always achieve that there are no formulas to the left of |-. Most deductive systems in use are therefore systems which test whether, for some given calculus and some given formula F, it holds that |- F (affirmative proof ), or dually, that |- -F= false (proof by contradiction).

The field in which such systems are developed, studied and applied is called automated deduction (AD). It has applications in any field where reasoning of any kind is relevant, which actually is most of science. AD’s first application was to Mathematics, for which historical reason the field is also known as automated theorem proving (ATP).

2. Issues In AD

Deductive systems have been developed for numerous different calculi with different formal languages and different rule sets. A very popular language is a version of first-order logic, called clausal logic. It uses sets of clauses like the three clauses in our apes example (which actually form four clauses, since presenting the set in the form ¬ F logically splits the last clause into the assumption → A with an empty premise and the denial of the conclusion, i.e., ¬ H or, equivalently, H → with an empty conclusion). In general, a clause may contain a conjunction of atoms in the premise and a disjunction of atoms in the conclusion. A correct and complete calculus based on clause sets is given by (essentially) the single rule of resolution in its general form. Resolution allows the elimination of intermediate literals even if they are not exactly identical but can be made identical by replacing variables in the atoms by functional terms, a process known as unification.

A deductive system based on resolution works as a saturation process. It takes the given clause set, and iteratively applies resolution until the so-called empty clause → (no premise, no conclusion, representing false) is obtained which forms the criterion for the validity of the inference represented by the input. The advantage of this type of system is the simplicity of the data-structures involved (clause sets) and the operations performed at each iteration (resolution). The problem is that, without additional constraints, the system produces relevant and irrelevant intermediate results alike, and for hard problems is often drowned in up to billions of generated clauses. An irrelevant intermediate result in our earlier example might be that ‘apes have eyes,’ on the basis of the additional knowledge that ‘mammals have eyes,’ when our only interest is in the question about hair. Strategies (like the so-called set-of-support strategy) to some extent help to reduce the amount of irrelevant clauses generated.

Alternatives to this saturation-based approach are the goal-oriented tableaux-based deductive systems. Human proofs, i.e., chains of inferences, may be regarded as tree-like structures, or (closed) tableaux, which in each branch start out from an obviously valid fact. The basic data-structure of tableaux-based systems is a (not necessarily closed) tableau. Starting with the tableau consisting of the (denial of the) given formula, the tableau is extended at each iteration with the goal of closing it. The data-structure (tableau) and the operations (extension of tableau) are more complicated than those in the saturation-based systems, which complicates the system development. But the approach allows a more goal-oriented fine-tuning of the search for the final proof and therefore is able to avoid some of the redundancy involved in resolution systems. At the time of writing, both approaches have reached about the same performance levels.

Systems based on the connection method may be regarded as a compactly coded form of tableaux systems. In this method, all information coded by a tableau is attached to the parts of the given formula in an extremely condensed form as structural information. Starting with an initial structure of this kind, only the structure is modified at each iteration until a certain final structure is reached signaling validity of the formula; the latter itself is not changed at all in the process.

Research in AD pursues all three kinds of approach, with the focus in each case being on eliminating redundancy. This can be achieved in various ways. One way consists in refined calculi in terms of the rule sets used. For instance, the application of resolution may be restricted in many ways without sacrificing completeness (e.g., linear resolution). Another way to reduce redundancy consists in applying various strategies which guide the rule application. A third consists in performing several small steps as a single global step (e.g., hyperresolution) which again narrows the search space. A fourth involves global steps sanctioned by theories involved (such as equality theory). Finally, ever-improved software engineering techniques and faster machines contribute to a continuous enhancement of system performance.

3. Applications And References

Mathematics is a primary field of application for AD. Deductive systems have been applied to virtually all subdisciplines in Mathematics, and tens of thousands of theorems have been proved automatically. New proofs have been found automatically for known theorems as well as for conjectures never proved before by any human. For instance, a system called Otter/EQP in 1996 settled an important mathematical problem which had been open for sixty years.

AD techniques are further used in programming. For instance, the programming language PROLOG basically works as a deductive system. Systems which synthesize programs from descriptive specifications, like the system KIDS, involve strong deductive components. Another important application of AD techniques to programming consists in the verification of software or hardware. Entire chips as well as compilers have been proved correct this way.

AD techniques have spread out into all fields of science by way of so-called knowledge-based systems which encode knowledge of specific disciplines and allow the manipulation of such knowledge in a deductive way. In the CYC system, an entire encyclopedia of knowledge is encoded in this way.

Bibel (1993) is a special textbook on all aspects of deductive methods and systems. Bibel and Schmitt (1998) is a reader covering all modern deductive techniques, a number of very successful systems, and several important applications. Gabbay et al. (1991) is a handbook which includes deductive reasoning systems and other topics. Robinson and Voronkov (2000) is a handbook covering only deductive methods, techniques and systems. Ongoing research is reported in the Journal of Automated Reasoning (Kluwer Academic Publishers) and in the proceedings volumes (published by Springer Verlag) of the International Conferences on Automated Deduction, as well as in other journals and conferences.

Bibliography:

1. Bibel W 1993 Deduction: Automated Logic. Academic Press, London
2. Bibel W, Schmitt P H 1998 Automated Deduction—A Basis for Applications. Applied Logic Series. Kluwer, Dordrecht, Vol. I–III, The Netherlands
3. Gabbay D, Hogger C, Robinson J A (eds.) 1991 Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press, Oxford, UK
4. Voronkov A, Robinson J A (eds.) 2001 Handbook of Automated Reasoning. North Holland, Amsterdam