Automated Reasoning
6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings
Published on 22. June 2012
XIV, 568 pages
978-3-642-31365-3 (ISBN)
Description
This book constitutes the refereed proceedings of the 6th International Joint Conference on Automated Reasoning, IJCAR 2012, held in Manchester, UK, in June 2012. IJCAR 2012 is a merger of leading events in automated reasoning, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), FTP (International Workshop on First-Order Theorem Proving), and TABLEAUX (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods). The 32 revised full research papers and 9 system descriptions presented together with 3 invited talks were carefully reviewed and selected from 116 submissions. The papers address all aspects of automated reasoning, including foundations, implementations, and applications.
More details
Other editions
Additional editions
Bernhard Gramlich | Dale Miller | Ulrike Sattler
Automated Reasoning
6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings
Book
06/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Conference Organization
- Table of Contents
- Invited Talks
- Taking Satisfiability to the Next Level with Z3
- Some Applications of Z3
- Solving Recursive Predicates
- Solving Recursive Predicates Is an SMT Problem
- From Programs and Properties to SMT
- Generalized Property Directed Reachability
- Conclusions
- References
- Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics
- References
- SAT and SMT Are Still Resolution: Questions and Challenges
- References
- Full Papers and System Descriptions
- Unification Modulo Synchronous Distributivity
- Preliminaries
- A Set of Inference Rules for Elementary E-Unification
- From E-Unification Problems to Thue Systems
- The Dependency Graph
- Thue Systems Associated with E-Unification Problems
- Thue Systems and Intercell Turing Machines
- The Undecidability of Elementary E-Unification
- Conclusion
- References
- SAT Encoding of Unification in ELHR+ w.r.t. Cycle-Restricted Ontologies
- Introduction
- The Description Logics EL, EL+, and ELHR+
- Unification
- Subsumption w.r.t. EL+- and ELHR+-Ontologies
- Reduction of Unification w.r.t. Cycle-Restricted ELHR+-Ontologies to SAT
- Conclusions
- References
- UEL: Unification Solver for the Description Logic EL - System Description
- Motivation
- EL and Unification in EL
- Things Not Mentioned in the Theoretical Papers
- The System UEL and How to Use It
- An Example
- References
- Effective Finite-Valued Semantics for Labelled Calculi
- Introduction
- Preliminaries
- Canonical Labelled Calculi
- Partial Non-deterministic Matrices
- Introducing PNmatrices
- Decidability
- Minimality
- Finite PNmatrices for Canonical Labelled Systems
- Proof-Theoretic Applications
- Strong Analyticity
- Strong Cut-Admissibility
- Conclusions and Further Research
- References
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic
- Introduction
- Preliminary Results
- Background and Notations
- Convex Polytopes with an Infinite Number of Integer Points
- Intersection with an Affine Subspace
- Constant Positive Linear Combinations of Affine Forms
- The Fourier-Motzkin Procedure
- Computing the Linear Combinations Using a Simplex
- Soundness, Completeness, and Termination
- The Decision Procedure
- The Algorithm
- Soundness, Completeness, and Termination
- Experimental Results
- Conclusion and Future Works
- References
- How Fuzzy Is My Fuzzy Description Logic?
- Introduction
- Preliminaries
- Mathematical Fuzzy Logic
- The Fuzzy Description Logic -SHOI
- Properties of t-Norms without Zero Divisors
- The Crisp Model Property
- Consistency and Satisfiability
- Subsumption and Instance Checking
- Conclusions
- References
- Truthful Monadic Abstractions
- Introduction
- Base Logic
- Truthfulness
- From Predicates to Monadic Predicates
- From Terms to Monadic Terms
- From Intuitionistic to Classical Logic
- Examples
- Experimental Results
- Conclusion and Future Work
- References
- Satallax: An Automatic Higher-Order Prover
- Introduction
- Preliminaries
- Basic Search Procedure and Implementation
- Flags
- Conclusion and Future Work
- References
- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation
- Introduction
- Formal Preliminaries
- Strong Amalgamation and Quantifier-Free Interpolation
- Modularity of Quantifier-Free Interpolation
- Equality Interpolation and Strong Amalgamation
- Equality Interpolation at Work
- A Comparison with the Notion of Equality Interpolation in ym
- An Interpolation Algorithm for Combinations of Theories
- Interpolating Metarules
- A Quantifier-Free Interpolating Algorithm
- Conclusion and Related Work
- References
- SPARQL Query Containment under RDFS Entailment Regime
- Introduction
- Preliminaries
- RDF(S)
- SPARQL
- -Calculus
- RDF Graphs as Transition Systems
- Encoding SPARQL Queries
- Query Containment under RDFS Entailment
- Encoding the RDFS Semantics Approach
- Query Rewriting Approach
- Encoding the Schema Approach
- Complexity
- Conclusion
- References
- Automated Verification of Recursive Programs with Pointers
- Introduction
- Heaps in Dynamic Logic
- Programs
- Strongest Postconditions of Assignments
- Generation of Verification Conditions
- Deciding Entailment with Semantic Tableaux
- Example Runs of Prototype Implementation
- Conclusions and Future Work
- References
- Security Protocols, Constraint Systems, and Group Theories
- Introduction
- Preliminaries
- Terms
- Group Theories
- Group Theories Define Rings
- Constraint Systems
- Definitions
- Satisfiability and Equivalence Problems
- Towards Simple Constraint Systems
- Encoding Solutions into Systems of Equations
- General Constraint Systems
- Simple Constraint Systems
- Applications and Discussion
- References
- Taming Past LTL and Flat Counter Systems
- Introduction
- Flat Counter Systems and Its LTL Dialect
- Counter Systems
- Linear Temporal Logic with Past and Arithmetical Constraints
- Stuttering Theorem for PLTL[Ø]
- Fundamental Structures: Minimal Path Schemas
- Minimal Path Schemas
- Complexity Results
- Model-Checking PLTL[C] over Flat Counter Systems
- Characterizing Runs by System of Equations
- Elimination of Arithmetical Constraints and Disjunctions
- Main Algorithm
- Conclusion
- References
- A Calculus for Generating Ground Explanations
- Introduction
- Preliminaries
- A Calculus for Handling Abducible Constants
- Completeness of the Calculus
- A Generation of Explanations
- A Termination Result for SPA
- Discussion
- References
- EPR-Based Bounded Model Checking atWord Level
- Introduction
- Translation
- Encoding Hardware Specifications into FOL
- Encoding of Bit-Vectors and Memories
- Encoding of Bit-Vector Operations
- Encoding of the Transition Relation
- Encoding of Initial and Final State Constraints
- Encoding the BMC Problem
- Back to EPR
- Unrolling Addresses
- Pre-processing and Clausification
- Other Optimizations in the Encoding
- Incremental Bounds
- Benchmarks and Experimental Results
- Comparison of Encodings of Bit-Ranges
- Comparison with SAT-Based BMC
- Conclusions and Future Work
- References
- Proving Non-looping Non-termination Automatically
- Introduction
- Pattern Rules
- Creating Pattern Rules
- Using Equivalence of Pattern Terms
- Modifying Pattern Rules by Instantiation and Narrowing
- Detecting Non-termination
- A Strategy to Prove Non-termination Automatically
- Evaluation and Conclusion
- References
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Introduction
- Z-TRSs
- Inductive Theorem Proving with Z-TRSs
- Inductive Theorem Proving as a Decision Procedure
- Simple Decidable Conjectures
- Decidable Conjectures with Nesting
- Implementation and Evaluation
- Conclusions
- References
- Combination of Disjoint Theories: Beyond Decidability
- Introduction
- Notations
- Combining Models
- Combinations: Decidable Theories and Beyond
- Combining a Decidable and an Arbitrary Theory
- Parallel Refutation of a Union of Disjoint Theories
- Conclusion
- References
- Automated Analysis of Regular Algebra
- Introduction
- Dioids, Powers and Finite Sums
- Conway's Classical Axioms
- Boffa's Axioms
- Conway's Conjectures
- Kozen's Kleene Algebras
- Salomaa's Axioms
- Soundness
- Relative Completeness
- Conclusion
- References
- d-Complete Decision Procedures for Satisfiability over the Reals
- Introduction
- SMT with Type 2 Computable Functions
- Basics of Computable Analysis
- Bounded SMT over RF
- The Bounded -SMT Problem
- -Completeness of the DPLL"426830A ICP"526930B Framework
- Interval Constraint Propagation
- Handling ODEs
- DPLL"426830A ICP"526930B
- Applications
- Conclusion
- References
- BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics
- Introduction
- Related Work
- Syntax and Semantics of Bi-Intuitionistic Tense Logics
- A BDD Perspective of the Finite Model Method
- A Better Basis for Wf
- Constructing the Maximal Relation
- Using max to Construct Wf
- Extension to Bi-Intuitionistic Logic BiInt
- Extension to Bi-Intuitionistic Tense Logic BiKt
- Optimisations
- Experimental Results
- Conclusion and Further Work
- References
- From Linear Temporal Logic Properties to Rewrite Propositions
- Introduction and Context
- Preliminaries and Problem Statement
- Rewrite Words and Maximal Rewrite Words
- Defining Temporal Semantics on Rewrite Words
- Rewrite Propositions and Problem Statement
- Building Translation Rules
- Overview and Intuitions of the Translation
- Weak and Strong Semantics for LTL
- Girdling the Future: Signatures
- The Translation Rules
- Conclusions and Perspectives
- References
- Tableaux Modulo Theories Using Superdeduction
- Introduction
- From Axioms to Superdeduction Rules
- Superdeduction Rules for the B Set Theory
- Implementation and Benchmarks
- Conclusion
- References
- Solving Non-linear Arithmetic
- Introduction
- Preliminaries
- An Abstract Decision Procedure
- Producing Explanations
- Cylindrical Algebraic Decomposition
- Projection-Based Explanations
- Related Work and Experimental Results
- Conclusion
- References
- Inprocessing Rules
- Introduction
- Preliminaries
- Clause Elimination and Addition
- Notions of Redundancy
- Extended Notions of Redundancy
- Inprocessing as Deduction
- Rules of Inprocessing
- Instantiating the Rules Based on RAT
- Solution Reconstruction
- Capturing SAT Solving Techniques with the Inprocessing Rules
- Conclusion
- References
- Logical Difference Computation with CEX2.5
- Introduction
- Preliminaries
- The CEX2.5 System
- Experimental Results
- References
- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
- Introduction: Formal Mathematics and Its AI Methods
- Premise Selection Algorithms
- Premise Selection Setting
- Learning-Based Ranking Algorithms
- Other Algorithms Used in the Evaluation
- Techniques Not Included in the Evaluation
- Machine Learning Evaluation Metrics
- Evaluation
- Evaluation Data
- Machine Learning Evaluation - Comparison of Predictions with Known Proofs
- ATP Evaluation
- Combining Premise Rankers
- Conclusion and Future Work
- References
- Branching Time? Pruning Time!
- Introduction
- Branching Time
- Playing Time
- Pruning Time
- Annotations and Their Rules
- Truncating Infinite Trees
- Proving Time
- Conclusion
- References
- New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants
- Introduction
- Preliminaries
- Typed System and Single Homomorphism
- Correctness
- Complexity
- General Algorithm
- Algorithm Presentation
- Label Variables
- Soundness and Completeness
- Graph and SLP Operations
- Complexity
- References
- Reachability Analysis of Program Variables
- Introduction
- Operational Semantics
- Reachability
- Reachability Analysis
- Experiments
- Conclusion
- References
- Playing Hybrid Games with KeYmaera
- Introduction
- Hybrid Programs and
- Proof Rules for
- Case Study: Robotic Factory Automation
- Related Work
- References
- The QMLTP Problem Library for First-Order Modal Logics
- Introduction
- Obtaining and Using the Library
- Contents of the QMLTP Library
- The QMLTP Domain Structure
- Modal Problem Status and Difficulty Rating
- Naming, Syntax and Presentation
- Tools and Prover Database
- Conclusion
- References
- Correctness of Program Transformations as a Termination Problem
- Introduction
- Calculi and Program Transformations
- Proving Correctness of Program Transformations
- Abstract Reduction Sequences
- Rewriting by Forking and Answer Diagrams
- Proving Convergence Preservation
- A Rewriting System with Finitely Many Rules
- Encoding ARSs and Sets of Diagrams as ITRSs
- Conclusion
- References
- Fingerprint Indexing for Paramodulation and Rewriting
- Introduction
- Background
- Fingerprint Indexing
- Implementation
- Experimental Results
- Conclusion
- References
- Optimization in SMT with LA(Q) Cost Functions
- Introduction
- Optimization in SMT(LA(Q)T)
- Procedures for OMT(LA(Q)) and OMT(LA(Q)T)
- An Offline Schema for OMT(LA(Q))
- An Inline Schema for OMT(LA(Q))
- Extensions to OMT(LA(Q)T)
- Experimental Evaluation
- Comparison on LGDB Problems
- Comparison on SMT-LIB Problems
- Conclusions and Future Work
- References
- Synthesis for Unbounded Bit-Vector Arithmetic
- Introduction
- Preliminaries
- Quantifier-Free Presburger Arithmetic with Bit-Vector Logical Operators
- Sequential Circuits
- Translations between QFPAbit and Sequential Circuits
- Reduction from QFPAbit to Sequential Circuits
- Reduction from Sequential Circuits to QFPAbit
- From Specification Circuits to Transducer Circuits
- Implementation of C', and as Circuits
- Constructing Transducer as a Composition of Transducers for Sub-formulas
- Conclusion
- References
- Extended Caching, Backjumping and Merging for Expressive Description Logics
- Motivation
- Preliminaries
- Dependency Tracking
- Extended Caching and Backtracking
- Dependency Directed Backtracking
- Unsatisfiability Caching
- Dependency Backtracing
- Optimised Merging
- Evaluation
- Conclusions
- References
- KBCV - Knuth-Bendix Completion Visualizer
- Introduction
- Features
- Normal Mode
- Expert Mode
- Equational Logic and Certification
- Implementation and Experiments
- Conclusion
- References
- A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance
- Introduction
- Preliminaries
- The Algorithm
- Experimental Evaluation
- References
- Stratification in Logics of Definitions
- Introduction
- The Logic LD
- Examples
- A Ground Proof System with Recursive Definitions
- Simulating Cut Reductions of LD in LD
- Cut-Elimination for a Positive Fragment of LD
- Related and Future Work
- References
- Diabelli: A Heterogeneous Proof System
- Introduction
- Heterogeneous Reasoning Components
- The Diagrammatic Reasoner
- The Sentential Reasoner - Isabelle
- Integration of Diagrammatic and Sentential Reasoners
- Interpretation of Spider Diagrams in Isabelle/HOL
- Translation of Isabelle/HOL to Spider Diagrams
- Architecture of Diabelli
- General Observations
- References
- Author Index
