×

Handbook of logic in artificial intelligence and logic programming. Vol. 2: Deduction methodologies. (English) Zbl 0810.68005

Oxford: Clarendon Press. xv, 511 p. £55.00 /hc (1994).
[The articles of this volume will not be indexed individually.]
This book presents many deduction methodological available for various AI applications, especially for automated reasoning. The book covers the following topics: (1) logic for automation, (2) unifiction theory, (3) mathematical induction, (4) higher-order logic, (5) meta-languages, reflection principle, self-reference, (6) classical vs nonclassical logic (the universality of classical logic).
Topic 1 (pp. 1-40), by L. Wos and R. Veroff, deals with logical tools for automated reasoning. The strong point is the clause language paradigm with a variety of inference rules, diverse strategies and additional procedures. The use of the clause language paradigm helps to solve open questions of finite semigroups, equivalential calculus, combinatory logic, and sentential calculus. The relationship between the clause language paradigm and logic programming approaches is formulated and analyzed.
Topic 2 (pp. 41-125), by F. Baader and J. Siekmann, is devoted to the analysis of unification frequently used in AI systems. The original motivation for considering unification of uninterpreted terms in resolution theorem-proving and term rewriting is described. Besides Robinson’s unification algorithm also some other algorithms are outlined or derived. Unification results for special theories are presented. A generalization of unification for whole classes of theories is given. Syntactic and semantic unification approaches are considered, and the combination problem to overcome their drawbacks is formulated. A decomposition algorithm is constructed whose output is a finite set of pairs of equational theories. At the end, generalizations of unification are presented, e.g., higher-order unification, unification in sort theories, constraint solving, and some applications are mentioned (e.g., databases, expert systems, beliefs and modality, etc.).
Topic 3 (pp. 127-228), by C. Walther, starts with introducing basic terms and admissible specifications (data structures, theorem proving, induction, expanded theories). Inductive axioms and induction heuristic for selecting such axioms are defined. How to increase the effectiveness of the heuristic modifications of induction axioms by domain and range generalization or by separation is considered. The problem of proving well-foundedness of certain relations is analyzed. Well-foundedness proofs are also required to prove the termination of algorithms. To prove arbitrary induction formulas, a basic theorem-prover as a subsystem of the whole induction system is defined. Some specific techniques, such as symbolic evaluation, applying induction hypotheses, and using lemmata, are developed for evaluating or proving induction formulas. Finally, a generalization of induction formulas is considered, and inverse inference rules, as a mechanism for obtaining generalized formulas, is defined.
Topic 4 (pp. 229-321) by D. Leivant, brings essential issues and facts of higher-order logic. In the second part it contains also slightly more technical concepts and issues. The canonical semantics of second and higher-order logics are defined, and proof theory of the former is described. The question whether second and higher-order logics are genuine logics, and the view to higher-order logics as mathematical theories are discussed. Some usual options for restricting second-order logic are presented and the relationship between higher-order logic and set theory plus mathematical analysis is discussed. Some relations between higher-order logic and programming or computing are described.
The chapter with topic 5 (pp. 323-358) by D. Perlis and V. S. Subrahmanian, is devote to self-reference, a very important attribute of AI systems. Many issues surrounding self-reference in AI are presented, especially those related to nonmonotonicity, reification, an intentionality. Natural concomitants of self-reference, such as meta- language and reflection principle, are discussed. The positive problem of reflection together with the negative one are formulated, and the fixed- point techniques for studying changes of systems is described. As for applications, ideal and pseudo-ideal approaches to knowledge are presented and supported by fundamental theorems. Another application concerns meta-logic programming based on Prolog with the binary predicate symbol demo. As an important topic for future development of nonclassical reasoning, the relationship between syntactic symbolics and semantically assigning a meaning is shortly discussed.
The last chapter (pp. 359-500) by D. M. Gabbay, deals with the universality of classical logic and many versions of its applications. First, the fundamental notion of a logical system is discussed, then, defined in terms of consequence relations, or as an algorithmic proof system, or in terms of algorithmically structured consequence relations, or as a labelled deductive system, or even as an aggregated system, it is considered to be a practical reasoning system. A methodology of constructing a nonclassical logic for application is given: two case studies – one for temporal logic and the second for priority logic – are described. An algebraic version of the labelled deduction system (LDS) is defined and its semantic translation into algebraic classical logic is accomplished. LDS is said to be the best logical system for practice; its advantages/limitations are specified. It is shown that linking the labels of the algebra in LDS with formulas can be done for any two predicate systems within predicate logic. As a general mechanism of linking two languages, namely a first-order language \(G\) and a predicate language \(L\), the meta-language HFP (of Hereditarily Finite Predicates) is discussed in detail.

MSC:

68-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science
03-00 General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to mathematical logic and foundations
03B80 Other applications of logic
68T27 Logic in artificial intelligence

Citations:

Zbl 0804.03017
PDFBibTeX XMLCite