| Extended Abstracts of Invited Lectures |
| Microprocessor Verification Using Efficient Decision Procedures for a Logic of `zEquality with Uninterpreted Functions / Randal E. Bryant ; Miroslav N. Velev |
| Comparison |
| Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison / Fabio Massacci |
| DLP and FaCT / Peter F. Patel-Schneider ; Ian Horrocks |
| Applying an <$$$> ABox Consistency Tester to Modal Logic SAT Problems / Volker Haarslev ; Ralf Moller |
| KtSeqC: System Description / Vijay Boyapati ; Rajeev Gore |
| Abstracts of Tutorials |
| Automated Reasoning and the Verification of Security Protocols |
| Proof Confluent Tableau Calculi / Reiner Hähnle ; Bernhard Beckert |
| Contributed Research Papers |
| Analytic Calculi for Projective Logics / Matthias Baaz ; Christian G. Fermüller |
| Merge Path Improvements for Minimal Model Hyper Tableaux / Peter Baumgartner ; J.D. Horton ; Bruce Spencer |
| CLDS for Propositional Intuitionistic Logic / Krysia Broda ; Dov Gabbay |
| Intuitionisitic Tableau Extracted / James Caldwell |
| A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification / Domenico Cantone ; Calogero G. Zarba |
| Bounded Contraction in Systems with Linearity / Agata Ciabattoni |
| The Non-associative Lambek Calculus with Product in Polynomial Time / Philippe de Groote |
| Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization? / Stéphane Demri |
| Cut-Free Display Calculi for Nominal Tense Logics / Rajeev Goré |
| Hilbert's Epsilon-Terms in Automated Theorem Proving / Martin Giese ; Wolfgang Ahrendt |
| Partial Functions in an Impredicative Simple Theory of Types / Paul C. Gilmore |
| A Simple Sequent System for First-Order Logic with Free Constructors / Jean Goubault-Larrecq |
| linTAP: A Tableau Prover for Linear Logic / Heiko Mantel ; Jens Otten |
| A Tableau Calculus for a Temporal Logic with Temporal Connectives / Wolfgang May |
| A Tableaux Calculus for Pronoun Resolution / Christof Monz ; Maarten de Rijke |
| Generating Minimal Herbrand Models Step by Step / Heribert Schütz |
| Tableau Calculi for Hybrid Logics / Miroslava Tzakova |
| Full First-Order Free Variable Sequents and Tableaux in Implicit Induction / Claus-Peter Wirth |
| Contributed System Descriptions |
| An Interactive Theorem Proving Assistant / Ulrich Endriss |
| A Time Efficient KE Based Theorem Prover |
| Strategy Parallel Use of Model Elimination with Lemmata - System Abstract - / Andreas Wolf ; Joachim Draeger |
| Author Index |
| Extended Abstracts of Invited Lectures |
| Microprocessor Verification Using Efficient Decision Procedures for a Logic of `zEquality with Uninterpreted Functions / Randal E. Bryant ; Miroslav N. Velev |
| Comparison |
図書
