Automated Deduction -- CADE-23

Name: Automated Deduction -- CADE-23 | 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 -- August 5, 2011, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 -- August 5, 2011, Proceedings

Nikolaj Bjørner Viorica Sofronie-Stokkermans(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. Juli 2011

XIII, 508 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-22438-6 (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
Organization
Contents
The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond
Advances in Proving Program Termination and Liveness
Translating between Language and Logic: What Is Easy and What Is Difficult
Introduction
The Language of Mathematics
GF in a Nutshell
Abstract and Concrete Syntax
Parametrization
Multilinguality
Grammar Engineering
Baseline Translation for the Core Syntax of Logic
Abstract Syntax
Concrete Syntax
The Lexicon
Ambiguity
Beyond the Baseline Translations: Easy Improvements
Extended Abstract Syntax
From Extended Syntax to Core Syntax
From Core Syntax to Extended Syntax
Verbal vs. Symbolic
The Limits of Known Techniques
The Dynamicity of Language
The Structure of Proof Texts
Projects
Conclusion
References
ASASP: Automated Symbolic Analysis of Security Policies
Introduction
Background on Administrative Access Control
ASASP: Architecture, Implementation, and Experiments
Conclusions and Future Work
References
Backward Trace Slicing for Rewriting Logic Theories
Introduction
Preliminaries
Rewriting Modulo Equational Theories
Backward Trace Slicing for Elementary Rewrite Theories
Labeling Procedure for Rewrite Theories
Backward Tracing Relation
The Backward Trace Slicing Algorithm
Backward Trace Slicing for Extended Rewrite Theories
Dealing with Collapsing and Nonleft-Linear Rules
Built-in Operators
Associative-Commutative Axioms
Experimental Evaluation
Conclusion and Related Work
References
Deciding Security for Protocols with Recursive Tests
Introduction
Models for Security Protocols
Messages
Intruder Capabiblities
Constraint Systems
Example: the SMNDP Protocol
Constraint Solving Procedure
Simplification Rules
A Basis for Deducible Terms
Link-Based Recursive Languages
Routing Protocols
Mapping-Based Languages
Decision Procedure
Conclusion
References
The Matita Interactive Theorem Prover
The System
Proof Authoring
Formalizations
References
Unification in the Description Logic EL without the Top Concept
Introduction
The Description Logics EL and EL-T
Unification in EL and EL-T
An EL-T-Unification Algorithm
PSpace-Hardness of EL-T-Unification
Conclusion
References
Model Evolution with Equality Modulo Built-in Theories
Introduction
Preliminaries
Contexts and Constrained Clauses
Core Inference Rules
Model Construction, Redundancy and Static Completeness
The MEE(T) Calculus
Soundness and Special Cases
Conclusions
References
Blocked Clause Elimination for QBF
Introduction
Preliminaries
Preprocessing Techniques for QBF
Quantified Blocked Clause Elimination
Definition
Discussion
Extensions
Experimental Evaluation
Conclusion and Future Work
References
Extending Sledgehammer with SMT Solvers
Introduction
Sledgehammer
The SMT Proof Method
Combining Sledgehammer and SMT
Relevance Filtering
SMT Solver Invocation
Proof Reconstruction
Redistribution and Distribution
Experiment: Generation of Weights and Triggers
Example
Evaluation
Conclusion
References
Automated Cyclic Entailment Proofs in Separation Logic
Introduction
Syntax and Semantics
Cyclic Proofs of Separation Logic Entailments
Implementation of the Cyclic Prover
Representation of Pre-proofs
Soundness of the Implementation
Automated Proof Search
Experimental Performance
Related Work
Conclusions and Future Work
References
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
Introduction
Preliminaries
Mapping into SAT
States and Successors
Implementation
Results and Examples
Related Work
Conclusion
References
Experimenting with Deduction Modulo
Deduction Modulo
Extending Deductive Systems with Rewriting
Ordered Polarized Resolution Modulo
Technical Details
iProver
Input Files
Clause Generation by Narrowing
Simplifications
Benchmarks
Comparison with Other Calculi
Comparison of Rewriting Implementations
Conclusion
References
Heaps and Data Structures: A Challenge for Automated Provers
Introduction
The Quest for Fast Automated Provers
The Challenge
Contributions
Heap Encodings
Type-Safe C
Multiply-Linked List Benchmark Family
Experiments
Comparing ATPs with SMT Solvers
Guiding SMT Solver with Patterns
Scaling Up
Interpretation of the Results
Checking Real-World Verification Examples
Related Work
Conclusion
References
Optimized Query Rewriting for OWL 2 QL
Introduction
Preliminaries
The Rapid Algorithm
Atom Unfolding Sets
Atom Function Sets
Query Shrinking
Query Unfolding
Implementation
Evaluation
Conclusions
References
Sort It Out with Monotonicity
Introduction
Monotonicity Calculus for First-Order Logic
Monotonicity in an Unsorted Setting
Monotonicity in a Many-Sorted Setting
A Simple Calculus for Monotonicity Inference
Improved Calculus
Monotonicity Inference Rules of the Improved Calculus
NP-Completeness of the Improved Calculus
Monotonox: Sorted to Unsorted Logic and Back Again
Monotonicity Inference with Monotonox
Translating Sorted to Unsorted Logic
Translating Unsorted to Sorted Logic
Results
Conclusions and Future Work
References
Exploiting Symmetry in SMT Problems
Introduction
Notations
Defining Symmetries
SMT with Symmetries: An Algorithm
SMT with Symmetries: An Example
Experimental Results
Conclusion
References
Compression of Propositional Resolution Proofs via Partial Regularization
Introduction
The Resolution Calculus
Redundant Proofs
Algorithm LowerUnits
Algorithm RecyclePivotsWithIntersection
Experimental Evaluation
Related Work and Ideas for Future Work
Conclusions
References
Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms
Introduction
Definitions and Problem Statement
Algorithms
Experimental Results
Related Work
Conclusion
References
A Connection-Based Characterization of Bi-intuitionistic Validity
Introduction
Bi-intuitionistic Propositional Logic
Indexing Formulas
Bi-intuitionistic R-Graphs
R-Graph Reductions
Validity through R-Graphs
Characterization of Validity
Soundness and Completeness of the Characterization
Counter-Model Construction
Solving Admissibility Constraints
Variable Splitting
References
Automated Reasoning in ALCQ via SMT
Introduction
Background
The Description Logic ALCQ
Satisfiablity Modulo Theory with Cost Functions
Concept Satisfiability via SMT with Costs
Encoding ALCQ into SMT(C)
Partitioning Individuals
Smart Partitioning
Exploit Smart Partitioning in ALCQ2SMTC
Empirical Evaluation
References
Sine Qua Non for Large Theory Reasoning
Introduction
Symbol-Based Selection
Idea: Relevance
General Scheme
The Sine Selection
Idea
Examples
The Selection Algorithm in More Detail
Variations
Tolerance
Depth Limit
Generality Threshold
Experiments
Generality Threshold
Selected Formulas
Number of Iterations
Essential Parameters
Competition Performance
Related Work
Conclusion
References
Predicate Completion for non-Horn Clause Sets
Introduction
Preliminaries
Predicate Completion
The Predicate Completion Algorithm PC
Disunification-Based Quantifier Elimination
Solved Form Computation
Predicate Completion and Unique Herbrand Models
Conclusion
References
System Description: SPASS-FD
Introduction
Theoretical Background
Implementation
Testing and Optimizations
Conclusion
References
Cutting to the Chase Solving Linear Integer Arithmetic
Introduction
Preliminaries
The Abstract Search Procedure
Deriving Tight Inequalities
Main Procedure
Termination
Relevant Propagations
Strong Conflict Resolution
Experimental Evaluation
Conclusion
References
A Hybrid Method for Probabilistic Satisfiability
Introduction
Probabilistic Logic P-SROIQ
The Probabilistic Satisfiability Algorithm
Possible World Generation
Evaluation
Random Propositional Knowledge Bases
Probabilistic Extensions of Real Ontologies
Conclusion
References
Solving Systems of Linear Inequalities by Bound Propagation
Introduction
Preliminaries
Collapsing Inequalities
Bound Propagation Algorithm
Example
Correctness of BPA
Conclusions
References
On Transfinite Knuth-Bendix Orders
Introduction
Preliminaries
Transfinite KBO
TKBOs with Finite Subterm Coefficient Functions
Lower Bounds on Ordinals
Finite Term Coefficients
Arbitrary Weight Coefficients
TKBOs with Unrestricted Subterm Coefficient Functions
Notes on Implementation and Applications
Conclusion
References
Scala to the Power of Z3: Integrating SMT and Programming
Introduction
Implicit Computation Using Z3
Design and Implementation
Theory Plugins
Conclusions
References
Efficient General Unification for XOR with Homomorphism
Introduction
Basic Definitions
Exclusive OR with Homomorphism
Basic Notation
Rewriting System REXH
Inference System IEXH
Termination, Soundness and Completeness
Auxiliary Rules for Improving Efficiency
Conclusion and Future Work
References
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems
Introduction
Runtime Complexity of Term Rewriting
Dependency Tuples
DTProblems
DT Processors
Usable Rules Processor
Reduction Pair Processor
Dependency Graph Processors
Knowledge Propagation
Transformation Processors
Evaluation and Conclusion
References
Static Analysis of Android Programs
Introduction
Android Basics
Our Set of Static Analyses
Class Analysis for Android
Nullness Analysis for Android
Termination Analysis for Android
Conclusion
References
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs
Introduction
Preliminaries: Stochastic Processes
Stochastic Differential Equations
Stochastic Hybrid Programs
Stochastic Differential Dynamic Logic
Stochastic Calculus
Proof Calculus
Related Work
Conclusions
References
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving
Introduction
Preliminaries
RDF and OWL 2 Full
FOL, the TPTP Language, and ATP
Approach
Evaluation Setting
The FOL Axiomatization and RDF Graph Conversion
Test Data
Reasoners
Evaluation Environment
Evaluation Results
Language Coverage
Characteristic OWL 2 Full Conclusions
Scalability
Model Finding
Conclusions and Future Work
References
An Efficient Decision Procedure for Imperative Tree Data Structures
Introduction
Decision Procedure through an Example
Preliminaries
TREX: Logic of Trees with Reachability Expressions
Decision Procedure for TREX
Elimination of Function Updates
Elimination of Descendant Relations
Reduction to First-Order Logic
-Locality
Conclusion
References
AC Completion with Termination Tools
Introduction
Inference System
Implementation
Experiments
Conclusion
References
CSI - A Confluence Tool
Introduction
Techniques
Implementation
Evaluation
References
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken