edited by
Marcello D'Agostino Università di Ferrara, Italy Dov M. Gabbay Dept. of Computer Science, King's College, London, UK Reiner Hähnle Universität Karlsruhe, Germany Joachim Posegga Deutsche Telekom AG, Research Centre, Darmstadt, Germany
The tableau methodology, invented in the 1950's by Beth and
Hintikka and later perfected by Smullyan and Fitting, is today one of
the most popular proof theoretical methodologies. Firstly because it
is a very intuitive tool, and secondly because it appears to bring
together the proof-theoretical and the semantical approaches to the
presentation of a logical system.
The increasing demand for improved tableau methods for various logics
is mainly prompted by extensive applications of logic in computer
science, artificial intelligence and logic programming, as well as its
use as a means of conceptual analysis in mathematics, philosophy,
linguistics and in the social sciences.
In the last few years the renewed interest in the method of analytic
tableaux has generated a plethora of new results, in classical as well
as non-classical logics.
On the one hand, recent advances in tableau-based theorem proving have
drawn attention to tableaux as a powerful deduction method for
classical first-order logic, in particular for non-clausal formulas
accommodating equality.
On the other hand, there is a growing need for a diversity of
non-classical logics which can serve various applications, and for
algorithmic presentations of these logicas in a unifying framework
which can support (or suggest) a meaningful semantic interpretation.
From this point of view, the methodology of analytic tableaux seems to
be most suitable. Therefore, renewed research activity is being
devoted to investigating tableau systems for intuitionistic, modal,
temporal and many-valued logics, as well as for new families of
logics, such as non-monotonic and substructural logics.
The results require systematisation. This Handbook is the first
to provide such a systematisation of this expanding field. It contains
several chapters on the use of tableaux methods in classical logic,
but also contains extensive discussions on:
the uses of the methodology in intuitionistic logics
modal and
temporal logics
substructural logics, nonmonotonic and
many-valued logics
the implementation of semantic tableaux
a bibliography on analytic tableaux theorem proving.
The result is a solid reference work to be used by students and
researchers in Computer Science, Artificial Intelligence, Mathematics,
Philosophy, Cognitive Sciences, Legal Studies, Linguistics,
Engineering and all the areas, whether theoretical or applied, in
which the algorithmic aspects of logical deduction play a role.
