Automated Reasoning

Name: Automated Reasoning | 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings

Bernhard Gramlich Dale Miller Ulrike Sattler(Herausgeber*in)

Springer (Verlag)

Erschienen am 22. Juni 2012

XIV, 568 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-31365-3 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken