Automated Reasoning with Analytic Tableaux and Related Methods
Subtitle: International Conference, TABLEAUX'99, Saratoga Springs, NY, USA, June 7-11, 1999, Proceedings (Lecture Notes in Computer Science)
Edition: 1 edition
Publisher: Springer
Published: June 22, 1999
Language: eng
Format: Paperback
Number of pages: 323
ISBN-13: 9783540660866
Subjects: Knowledge-based systems / expert systems; Natural language & machine translation; Automata; Computers; Computers - General Information; Science/Mathematics; Artificial Intelligence - General; Expert Systems; General; Automated Deduction; Computers / Artificial Intelligence; Formal Systems Verification; Logic Reasoning Calculi; Tableaux Methods; Theorem Proving; Computer Science; Automatic theorem proving; Congresses
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>