Automated Reasoning with Analytic Tableaux and Related Methods
20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011, Proceedings
Published on 16. June 2011
VIII, 279 pages
978-3-642-22119-4 (ISBN)
Description
This book constitutes the refereed proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, held in Bern, Switzerland, in July 2011.The 16 revised research papers presented together with 2 system descriptions were carefully reviewed and selected from 34 submissions. The papers cover many topics in the wide range of applications of tableaux and related methods such as analytic tableaux for various logics, related techniques and concepts, related methods, new calculi and methods for theorem proving in classical and non-classical logics, as well as systems, tools, implementations and applications; all with a special focus on hardware and software verifications, semantic technologies, and knowledge engineering.
More details
Other editions
Additional editions
Kai Brünnler | George Metcalfe
Automated Reasoning with Analytic Tableaux and Related Methods
20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011, Proceedings
Book
06/2011
1st Edition
Springer
€53.49
Shipment within 5-7 days
Content
- Title
- Preface
- Organization
- Table of Contents
- On Interpolation in Decision rocedures
- Introduction
- A Framework of Definitions for Interpolation
- Transition Systems, Proofs and Interpolation Systems
- Propositional Interpolation Systems
- Interpolation and Equality
- Interpolation for Equality Sharing and DPLL(T )
- Future Work
- References
- First-Order Tableaux in Applications
- References
- Proof Theory and Algebra in Substructural Logics
- CSymLean: A Theorem Prover for the Logic CSL over Symmetric Minspaces
- The Logic CSL$
- The Theorem Prover CSymLean$
- Conclusion and Further Work
- References
- Schemata of SMT-Problems
- Introduction
- Preliminaries
- Syntax
- Semantics
- Extensions of the Language
- Undecidability
- Proof Procedure
- Enumerating Interpretations
- Termination
- Examples of Stably Decomposable Frames
- Literals Containing at Most One Index
- Ordered Theories
- Examples
- Conclusion
- References
- Kripke Semantics for Basic Sequent Systems
- Introduction
- Preliminaries
- Basic Systems
- Kripke Semantics
- Semantic Characterization of Analyticity
- Semantic Characterization of Strong Cut-Admissibility
- Further Research Topics
- References
- Hybrid and First-Order Complete Extensions of CaRet
- Introduction
- Preliminaries
- The Linear Hybrid Logic HyCaRet and Known Extensions of CaRet
- Automata for Visibly Pushdown Languages
- Expressiveness and Succinctness of 1-HyCaRet
- Decision Procedures for HyCaRet
- References
- Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders
- Introduction
- Propositional Neighborhood Logic
- Labeled Interval Structures and Satisfiability
- Decidability of PNL
- Tableau Systems for PNL
- Conclusions and Future Work
- References
- Craig Interpolation in Displayable Logics
- Introduction
- Display Calculus Fundamentals
- Interpolation: Nullary, Unary and Structure-Free Rules
- Interpolation: Binary Logical Rules
- Interpolation: Structural Rules
- Related and Future Work
- References
- A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders
- Introduction
- The Tableau Calculus
- Properties of the Calculus
- Concluding Remarks
- References
- Basic Constructive Connectives, Determinism and Matrix-Based Semantics
- Introduction
- Preliminaries
- Single-Conclusion Canonical Systems
- Non-deterministic Kripke-Style Semantics
- Deterministic Connectives
- Axiom-Expansion
- Invertibility of Rules
- Matrix-Based (Kripke) Semantics
- References
- On the Proof Complexity of Cut-Free Bounded Deep Inference
- Introduction
- Preliminaries
- The Depth-Change Trick
- Reducing Non-determinism
- Conclusions
- Applications to Sequent Calculi
- Bounded-Depth Systems Not Containing Cocontraction
- The Effect of Cocontraction on Proof Complexity
- References
- The Modal µ-Calculus Caught Off Guard
- Introduction
- The Modal µ-Calculus
- Tableaux for the Modal µ-Calculus
- A Decision Procedure Based on Tableaux
- Automata-Theoretic Machinery
- Reduction to Parity Game Solving
- Comparison
- References
- A Conditional Constructive Logic for Access Control and Its Sequent Calculus
- Introduction
- The Logic CondACL$
- Axiom System
- Semantics
- Soundness and Completeness
- A Sequent Calculus for CondACL$
- Termination and Complexity of SCondACL$
- OtherAxioms
- Related Work and Conclusions
- References
- A Tableau Calculus for a Nonmonotonic Extension of EL
- Introduction
- The Typicality Operator T, the Logic ELTmin and its Left Local Fragment
- The Tableau Calculus for Left Local ELTmin
- First Phase: The Tableaux Calculus TAB
- The Tableaux Calculus TAB
- Conclusions
- References
- Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics
- Introduction
- Preliminaries: Hybrid PDL
- Demos as a Syntactic Representation of Models
- The Decision Procedure
- Nominals
- Difference Modalities
- Tests
- Converse Actions
- Related Work
- References
- Cut Elimination for Shallow Modal Logics
- Introduction
- Preliminaries and Notation
- From Hilbert Systems to Sequent Systems
- Cut-Closure and Pseudo-Analytic Cut
- Cut Elimination Using Small Representations
- Proof Search in GR
- Applications: Exemplary Complexity Bounds
- Conclusion
- References
- A Non-clausal Connection Calculus
- Introduction
- The Clausal Connection Calculus
- Non-clausal Proof Search
- Non-clausal Matrices
- The Non-clausal Connection Calculus
- The Non-clausal Connection Calculus
- Basic Concepts
- The Calculus
- Correctness, Completeness and Complexity
- Correctness
- Completeness
- Complexity
- Optimizations and Extensions
- A Simplified Connection Calculus
- Optimizations
- Non-classical Logics
- Conclusion
- References
- #METTEL$ : A Tableau Prover with Logic-Independent Inference Engine
- Introduction
- Input Syntax
- Implementation Details
- Using METTEL$
- Concluding Remarks
- References
- A Hypersequent System for Gödel-Dummett Logic with Non-constant Domains
- Introduction
- Semantics and an Axiomatic System of Quantified LC
- The Hypersequent System HQLC
- Cut Elimination for HQLC
- Signature Weakening and Substitution
- Invertible and Admissible Rules
- Cut Elimination
- Soundness and Completeness of HQLC
- Related and Future Work
- References
- MaLeCoP Machine Learning Connection Prover
- Introduction
- Large-Theory Automated Reasoning
- Machine Learning in Large Theory ATP
- leanCoP: Lean Connection-Based Theorem Prover
- Why leanCoP
- The Basic leanCoP Procedure and its Parametrization
- The General Architecture
- The Concerns
- The Design
- MaLeCoP: Machine Learning Connection Prover
- The Theorem Prover
- The General Advisor and the External System
- Evaluation
- Dataset
- Results in Proof Shortening
- Solving New Problems
- Discussion, Future Work
- References
- Author Index
