Automated reasoning with analytic tableaux and related methods

This volume contains the papers presented at TABLEAUX’98, the International Conference on Analytic Tableaux and Related Methods, held on May 5-8, 1998 in Oisterwijk (conference centre Boschoord), near Tilburg, The Netherlands. This conference was a continuation of international workshops/conferences on Theorem Proving with Analytic Tableaux and Related Methods held in Laut- bach near Karlsruhe (1992), Marseille (1993), Abingdon near Oxford (1994), St. Goar near Koblenz (1995), Terrasini near Palermo (1996), and Pont- a-Mousson near Nancy (1997). Tableau methods have been found to be a convenient formalism for automating deduction in various non-standard logics as well as in classical logic. Areas of application include veri cation of software and computer systems, deductive - tabases, knowledge representation and its required inference engines, and system diagnosis. The conference brought together researchers interested in all aspects { theoretical foundations, implementation techniques, systems development, and applications { of the mechanization of reasoning with tableaux and related methods. From the 34 papers submitted, 17 original research papers and 3 original system descriptions were selected by the program committee for presentation at the c- ference and for inclusion in these proceedings, together with the invited lectures. Abstracts of the tutorials have also been included. These proceedings also c- tain the summary of the comparison of theorem provers for modal propositional logics, as part of the Tableaux’98 conference, together with the contributions of the persons who participated in this comparison. As before, Tableaux’98 attracted interest from many parts of the world with papers from many countries.