Automated reasoning with analytic tableaux and related methods

Más información sobre el libro

InhaltsverzeichnisExtended 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 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 Quantification. From K