Automated Reasoning with Analytic Tableaux and Related Methods

By Neil V. Murray

Subjects: Kunstmatige intelligentie, Congresses, Inteligencia artificial (computacao), Automatisches Beweisverfahren, Automatic theorem proving, Théorèmes, Automation, Démonstration automatique, Redeneren, Congrès, Logischer Schluss

Description: 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>