scientific article; zbMATH DE number 1395652

Authors

Publication date 31 January 2000

efficiency Handbook tableau method Tableau methods

Collections of articles of miscellaneous specific interest (00B15) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to mathematical logic and foundations (03-00) Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)

Review text

Table of Contents: ``Introduction by \textit{M. Fitting} (pp. 1-43); ``Tableau methods for classical propositional logic by \textit{M. D'Agostino} (pp. 45-123); ``First-order tableau methods by \textit{R. Letz} (pp. 125-196); ``Equality and other theories by \textit{B. Beckert} (pp. 197-254); ``Tableaux for intuitionistic logics by \textit{A. Waaler} and \textit{L. Wallen} (pp. 255-296); ``Tableau methods for modal and temporal logics by \textit{R. Goré} (pp. 297-396); ``Tableau methods for substructural logics by \textit{M. D'Agostino}, \textit{D. Gabbay} and \textit{K. Broda} (pp. 397-467); ``Tableaux for nonmonotonic logics by \textit{N. Olivetti} (pp. 496-528); ``Tableaux for many-valued logics by \textit{R. Hähnle} (pp. 529-580); ``Implementing semantic tableaux by \textit{J. Posegga} and \textit{P. Schmitt} (pp. 581-629); ``A bibliography on analytic tableaux theoren proving by \textit{G. Wrightson} (pp. 631-655); Index (pp. 657-670). The tableau method is a tool, not a subject, for investigations. It is easy, natural, and versatile as the above table of contents indicates. Unlike the work of the fouding fathers (Beth, Smullyan) in the 1950's, efficiency is a prominent aspect of the present day activity. All authors of this Handbook reflect this tendency: they first set up formal languages, then appropriate tableaux, prove soundness, completeness, etc. After that, they discuss efficiency, and present modifications and improvements of the tableau methods in this line. As the editors state, all the chapters are independent from one another and carry exellent references to activities in their areas. On the other hand, tables of contents are non-existent, and the index of the book is skimpy. So, this handbook is for the study of the chapter of the reader's interest, not for quick reference of definitions and facts. Below, we present short descriptions of the chapters, in a ``key word dropping style. ``Introduction, written by a senior statesman of the discipline, is pleasant reading. He gives a general idea of tableau methods, traces their genesis and developments (Gentzen, Beth, et al.), and also the scope that this book covers, including substructural and nonmonotonic logics as well as the efficiency aspect. ``Classical propositional logic is writtem with an eye on computational complexity and efficiency. The author dwells on the merits and faults of the tableau method with regard to these, and hence its modifications and improvements. He also makes comparisons with other methods such as natural deduction, truth table, resolution, Davis-Putnam procedure, and the KE-system. (The tableau method does not always come out to be the best.) ``First-order begins like an elementary logic textbook -- the formal language, Skolem form, Herbrand universe, etc. The meat of this chapter is the treatment of the free variable tableau method accompanied by unification, and the discussion of other calculi from the efficiency and the completeness point of view. For instance, connection tableaux produce answers quickly when they work, but the confluence property is not guaranteed. In ``Equality and other theories, free variable and universal formula tableau methods are introduced to promote efficiency. The author emphasizes the interaction between foreground and background reasoners, including incremental theory reasoning. He mentions, a number of times, the lack of a uniform recipe, which appears natural to the reviever, since word problems are \(E\)-unifications, and the Diophantine question (= Hilbert's 10th) falls in this area. The work in ``Intuitionistic logics is formulated in sequents rather than in tableaux. The authors present the calculus, LB, a modification of Gentzen's LJ. (It is identical with the calculus used by Maehara in his 1954 paper, as the authors note.) (The tableau in this chapter is composed of signed formulas, not of formulas themselves, and so it is synonymous with a sequent). They also formulate refutation trees, from which Kripke models can be produced easily. In connection with efficiency, they discuss permutabilities of inference rules, and term substitutions in connection with quantifier rules. In ``Modal and temproal logics, only propositional calculi are considered, but a great number of them. Besides the usual necessity interpretation of \(\square\), there is a calculus in which \(\square A\) is interpreted as `\(A\) is believed', so that \(\square A\to A\) is not valid. (Belief does not entail truth!) Some multi-modal logics have binary modal connectives like \(A\underline UB\), ``\(A\) is true until \(B\) becomes true. A labelled tableau is composed of \((\sigma::A)\)'s where \(A\) is a formula and \(\sigma\) represents worlds in which \(A\) is true. With respect to these calculi and tableaux, of course, the author discusses soundness, completeness, efficiency question, etc. He gives good accounts of ``intuition for axioms and rules. ``Substructural logics analyse the consequence relation. In Gentzen's sequent calculus, it was expressed by structural rules. And so, the logics in question are obtained by restricting or modifying these rules. They include relevance logic, BCK logic, (Lambek's) categorial logic, and linear logic. The authors of this chapter concentrate on the comparison of tableau and sequent approaches to relevance logic, and on labelled tableaux. The latter are the authors' speciality, and entail a uniform treatment of various logics. The authors introduce labelling algebras, and for logics of classical type information frames. ``Nonmonotonic logics are formulations of commonsense reasoning, which must jump to conclusions from available data. So, its logics are not monotonic: newly addad premisses may force the withdrawal of previous conclusions. The author groups the vast numbers of approaches into two: the fixed point approach (autoepistemic logics, default logics, etc.) and the semantic preference approach (minimal entailments). Tableau systems for these logics and entailments are set up and developed. But this chapter is more for reflections on and discussions about how to approach the subject, including the first-order case. ``Many-valued logics has more of survey character than introduction, in comparison with other chapters. Quite a number of notions, techniques, etc. (including integer programs) are commented upon, or at least mentioned, and so even a list of key words would be very long. The author emphasizes the interplay of model-theoretic and proof-theoretic considerations. A basic ingredient is the signed formula which is the pair of a formula and a truth value. (So, the disjunction of \(\langle A,t_i\rangle\), with one formula \(A\) and all truth values \(t_i\) is a generalization of the excluded middle of classical logic.) An extension which assigns a set of truth values, rather than one value, is ``a simple device but ``has far reaching consequences for the efficiency and generality of tableau methods, as the author demonstrates. ``Implementing semantic tableaux begins with a tutorial of a Prolog program, lean \(T^AP\), which is devised for this purpose. Then the authors discuss tableaux from the implementational viewpoint, including such aspects as tableaux as graphs, the compilation of tableaux, and the integration of lemmas into tableaux. ``A bibliography on analytic tableaux theorem proving. The author states that he has ``attempted to make this bibliography as comprehensive as possible with respect to published works relating automated reasoning with analytic tableaux. It carries about 200 items, with short comments to some.

Recommendations

Cited in

(33)

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4935259)