Automated Reasoning with Analytic Tableaux and Related Methods
International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, May 5-8, 1998, Proceedings
Published on 22. April 1998
Book
Paperback/Softback
X, 325 pages
978-3-540-64406-4 (ISBN)
Description
The volume presents 17 revised full papers and three system descriptions selected from 34 submissions; also included are several abstracts of invited lectures, tutorials, and system comparison papers. The book presents new research results for automated deduction in various non-standard logics as well as in classical logic. Areas of application include software verification, systems verification, deductive databases, knowledge representation and its required inference engines, and system diagnosis.
More details
Series
Language
English
Place of publication
Heidelberg
Germany
Publishing group
Springer Berlin
Target group
College/higher education
Professional and scholarly
Illustrations
biography
Dimensions
Height: 23.5 cm
Width: 15.5 cm
Weight
460 gr
ISBN-13
978-3-540-64406-4 (9783540644064)
DOI
10.1007/3-540-69778-0
Schweitzer Classification
Content
Extended Abstracts of Invited Lectures.- Philosophical Aspects of Computerized Verification of Mathematics.- A Science of Reasoning (Extended Abstract).- Model Checking: Historical Perspective and Example (Extended Abstract).- Comparison.- Comparison of Theorem Provers for Modal Logics - Introduction and Summary.- FaCT and DLP.- Prover KT4.- leanK 2.0.- Logics Workbench 1.0.- Optimised Functional Translation and Resolution.- Benchmark Evaluation of ?KE.- Abstracts of the Tutorials.- Implementation of Propositional Temporal Logics Using BDDs.- Computer Programming as Mathematics in a Programming Language and Proof System CL.- Contributed Research Papers.- A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results.- Hyper Tableau - The Next Generation.- Fibring Semantic Tableaux.- A Tableau Calculus for Quantifier-Free Set Theoretic Formulae.- A Tableau Method for Interval Temporal Logic with Projection.- Bounded Model Search in Linear Temporal Logic and Its Application to Planning.- On Proof Complexity of Circumscription.- Tableaux for Finite-Valued Logics with Arbitrary Distribution Modalities.- Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion.- Simplification and Backjumping in Modal Tableau.- Free Variable Tableaux for a Logic with Term Declarations.- Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux.- A Tableaux Calculus for Ambiguous Quantifiation.- From Kripke Models to Algebraic Counter-Valuations.- Deleting Redundancy in Proof Reconstruction.- A New One-Pass Tableau Calculus for PLTL.- Decision Procedures for Intuitionistic Propositional Logic by Program Extraction.- Contributed System Descriptions.- The FaCT System.- Implementation of Proof Search in the Imperative Programming Language Pizza.- p-SETHEO: Strategy Parallelism in Automated Theorem Proving.