Automated Reasoning with Analytic Tableaux and Related Methods

Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’99 Saratoga Springs, NY, USA, June 7–11, 1999 Proceedings<br />Author: Neil V. Murray<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-66086-6<br /> DOI: 10.1007/3-540-48754-9<br /><br />Table of Contents:<p></p><ul><li>Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions
</li><li>Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison
</li><li>DLP and FaCT
</li><li>Applying an
</li><li>KtSeqC : System Description
</li><li>Automated Reasoning and the Verification of Security Protocols
</li><li>Proof Confluent Tableau Calculi
</li><li>Analytic Calculi for Projective Logics
</li><li>Merge Path Improvements for Minimal Model Hyper Tableaux
</li><li>CLDS for Propositional Intuitionistic Logic
</li><li>Intuitionisitic Tableau Extracted
</li><li>A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification
</li><li>Bounded Contraction in Systems with Linearity
</li><li>The Non-associative Lambek Calculus with Product in Polynomial Time
</li><li>Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?
</li><li>Cut-Free Display Calculi for Nominal Tense Logics
</li><li>Hilbert’s ∈-Terms in Automated Theorem Proving
</li><li>Partial Functions in an Impredicative Simple Theory of Types
</li><li>A Simple Sequent System for First-Order Logic with Free Constructors
</li><li>linTAP : A Tableau Prover for Linear Logic</li></ul>