Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX &#039,99, Saratoga Springs, NY, USA, June 7-11, 1999 : proceedings

Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX’99 Saratoga Springs, NY, USA, June 7–11, 1999 Proceedings
Author: Neil V. Murray
Published by Springer Berlin Heidelberg
ISBN: 978-3-540-66086-6
DOI: 10.1007/3-540-48754-9

Table of Contents:

• Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions
• Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison
• DLP and FaCT
• Applying an
• KtSeqC : System Description
• Automated Reasoning and the Verification of Security Protocols
• Proof Confluent Tableau Calculi
• Analytic Calculi for Projective Logics
• Merge Path Improvements for Minimal Model Hyper Tableaux
• CLDS for Propositional Intuitionistic Logic
• Intuitionisitic Tableau Extracted
• A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification
• Bounded Contraction in Systems with Linearity
• The Non-associative Lambek Calculus with Product in Polynomial Time
• Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization?
• Cut-Free Display Calculi for Nominal Tense Logics
• Hilbert’s ∈-Terms in Automated Theorem Proving
• Partial Functions in an Impredicative Simple Theory of Types
• A Simple Sequent System for First-Order Logic with Free Constructors
• linTAP : A Tableau Prover for Linear Logic

Includes bibliographical references