Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’99 Saratoga Springs, NY, USA, June 7–11, 1999 Proceedings

Randal E. Bryant, Steven German, Miroslav N. Velev (auth.), Neil V. Murray (eds.)3540660860, 9783540660866

This book constitutes the refereed proceedings of the International Conference on Analytic Tableaux and Related Methods, TABLEAUX’99, held in Saratoga Springs, NY, USA, in June 1999.
The volume presents 18 revised full papers and three system descriptions selected from 41 submissions. Also included are system comparisons and abstracts of an invited paper and of two tutorials. All current issues surrounding mechanization of reasoning with tableaux and similar methods are addressed – ranging from theoretical foundations to implementation and systems development and applications, as well as covering a broad variety of logic calculi. As application areas, formal verification of software and computer systems, deductive databases, knowledge representation, and systems diagnosis are covered.

---

Table of contents :
Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions….Pages 1-13
Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison….Pages 14-18
DLP and FaCT….Pages 19-23
KtSeqC : System Description….Pages 24-29
Automated Reasoning and the Verification of Security Protocols….Pages 29-31
Proof Confluent Tableau Calculi….Pages 32-34
Analytic Calculi for Projective Logics….Pages 34-35
Merge Path Improvements for Minimal Model Hyper Tableaux….Pages 36-51
CLDS for Propositional Intuitionistic Logic….Pages 51-66
Intuitionisitic Tableau Extracted….Pages 66-82
A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification….Pages 82-96
Bounded Contraction in Systems with Linearity….Pages 97-112
The Non-associative Lambek Calculus with Product in Polynomial Time….Pages 113-128
Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?….Pages 128-139
Cut-Free Display Calculi for Nominal Tense Logics….Pages 140-155
Hilbert’s ∈ -Terms in Automated Theorem Proving….Pages 155-170
Partial Functions in an Impredicative Simple Theory of Types….Pages 171-185
A Simple Sequent System for First-Order Logic with Free Constructors….Pages 186-201
linTAP : A Tableau Prover for Linear Logic….Pages 202-216
A Tableau Calculus for a Temporal Logic with Temporal Connectives….Pages 217-231
A Tableau Calculus for Pronoun Resolution….Pages 232-246
Generating Minimal Herbrand Models Step by Step….Pages 247-262
Tableau Calculi for Hybrid Logics….Pages 263-277
Full First-Order Free Variable Sequents and Tableaux in Implicit Induction….Pages 278-292
An Interactive Theorem Proving Assistant….Pages 293-307
A Time Efficient KE Based Theorem Prover….Pages 308-313
Strategy Parallel Use of Model Elimination with Lemmata….Pages 313-318
….Pages 319-323