Automated Reasoning With Analytic Tableaux and Related Methods: International Conference, Tableaux'98, Oisterwijk, the Netherlands, May 5-8, 1998 : Proceedings: 1397 - Brossura

Tableaux'9 (1998 Oisterwijk, Netherlands); De Swart, Harrie

Brossura

ISBN 10: 3540644067 ISBN 13: 9783540644064

Casa editrice: Springer Verlag, 1998

Riassunto

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.

Su questo libro

Contenuti

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.

Dettagli dell?edizione

• Editore: Springer Verlag
• Data di pubblicazione: 1998
• Lingua: Inglese
• ISBN 10: 3540644067
• ISBN 13: 9783540644064
• Rilegatura: Copertina flessibile
• Numero edizione: 1
• Numero di pagine: 324
• Contatto del produttore: {language_tag:it_IT,value:"Springer Nature Customer Service Center GmbH; ProductSafety@springernature.com"}