Frontiers of Combining Systems

Name: Frontiers of Combining Systems | 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings

Carsten Lutz Silvio Ranise(Herausgeber*in)

Springer (Verlag)

Erschienen am 19. September 2015

XVII, 357 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-24246-0 (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

Intro
Preface
Organization
Abstracts of Invited Talks
Contents
Invited Talk
Free Variables and Theories: Revisiting Rigid E-Unification
1 Introduction
2 Background
2.1 Rigid E-Unification
2.2 Subterm Instantiation and Bounded Rigid E-Unification
2.3 Bounded Rigid E-Unification Formally
3 Semantically Solving BREU
3.1 Semantic Solvability in a First-Order Calculus
3.2 The Complexity of Semantic Solvability
4 Towards Bounded Rigid Theory Unification
5 Challenges and Conclusion
Description Logics
Decidable Description Logics of Context with Rigid Roles
1 Introduction
2 Basic Notions
3 Complexity of the Consistency Problem
4 The Case of EL: LM[[EL]] and EL[[LO]]
5 Conclusions
Adding Threshold Concepts to the Description Logic EL
1 Introduction
2 The Description Logic EL
3 The Logic EL(m)
4 The Membership Function deg
5 Reasoning in EL(deg)
6 Concept Similarity and Relaxed Instance Queries
7 Conclusion
Reasoning in Expressive Description Logicsunder Infinitely Valued Gödel Semantics
1 Introduction
2 Preliminaries
3 Automata for Complex Role Inclusions
4 The Reduction
5 Conclusions
References
Theorem Proving and Model Building
NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
1 Introduction
2 Preliminaries
3 Calculus
4 Soundness
5 Termination and Completeness
6 Related Work
7 Conclusion
First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
1 Introduction
2 Linear Shallow Monadic Horn Approximation
3 Lifting a Conflicting Core
4 Approximation Refinement
5 Summary
An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
1 Introduction
2 Background
2.1 The Satisfiability Problem
2.2 Partition Functions in SAT Solvers
2.3 Label Functions
3 The Instance Decomposition Model ID
4 Proof Format
5 Conclusion
Decision Procedures
Weakly Equivalent Arrays
1 Introduction
2 Notation
3 A Motivating Example
4 Weak Equivalences over Arrays
5 A Decision Procedure Based on Weak Equivalences
6 Extension to TAxDiff
7 Implementation and Evaluation
8 Conclusion and Future Work
A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
1 Introduction
1.1 Related Work
1.2 Formal Preliminaries
2 A Theory of Strings and Regular Language Membership
3 A Calculus for Constraint Satisfiability in TLR
4 Calculus Correctness
4.1 Termination
4.2 Correctness
4.3 Decidability
5 Conclusion and Further Work
Adapting Real Quantifier Elimination Methods for Conflict Set Computation
1 Introduction
2 Real Quantifier Elimination
2.1 Cylindrical Algebraic Decomposition
2.2 Virtual Substitution
3 Finding Conflict Sets
3.1 Conflict Sets and Linear Programming
3.2 Conflict Sets and Quantifier Elimination Optimization
4 Finding Conflict Sets via Redlog
5 Conclusion
Decision Procedures for Verification
A New Acceleration-Based Combination Framework for Array Properties
1 Introduction
2 Notation
3 Acceleratable Fragments
4 Acceleration Modules in Satisfiability Procedures
5 Applications to Imperative Programs
6 Conclusions and Future Work
Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata
1 Introduction
2 Spatial Families of Hybrid Automata
3 Verification Tasks
3.1 Safety Properties
3.2 Reduction to Satisfiability Checking
4 Automated Reasoning
5 Verification: Decidability and Complexity
6 Tool Support
7 Conclusions
Rewriting and Constraint Solving
A Completion Method to Decide Reachabilityin Rewrite Systems
1 Introduction
2 Polarized Rewrite Systems
3 Cut-Elimination
4 Ground Finite Rewrite Systems
5 Pushdown Systems
Axiomatic Constraint Systemsfor Proof Search Modulo Theories
1 Introduction
2 Ground Calculus and Examples
3 Constraint Structures
4 A System for Proof Search with Constraints
4.1 The Constraint-Producing Sequent Calculus LK?1
4.2 Instantiations and Compatibility with Constraints
4.3 Soundness and Completeness
5 Sequentialising
5.1 Definition of the Proof System
5.2 Soundness and Completeness
6 Relating LK?"526930B 1 to LK1
7 Implementation
8 Related Works and Further Work
Transformations between SymbolicSystems
Formalizing Soundness and Completeness of Unravelings
1 Introduction
2 Preliminaries
3 Formalizing Conditional Rewriting
4 Unravelings
5 Completeness of Unravelings
6 Soundness of Unravelings
7 Applying Unravelings to Confluence
8 Conclusion
Proofs and Reconstructions
1 Introduction
2 Reconstruction Workflow
3 Cut Machines
3.1 Validating the Model
3.2 Using the Model
3.3 Extending the Model
4 Framework
4.1 Proof Generation
4.2 Formula Interpretation
4.3 Proof Analysis and Transformation
4.4 Emulation of Inference Rules
4.5 Generating a Cut Program
4.6 Executing a Cut Program
5 Implementation
5.1 Evaluation
6 Related Work
7 Conclusions
Combination Methods
A Rewriting Approach to the Combination of Data Structures with Bridging Theories
1 Introduction
2 Preliminaries: Notations and Combinations
3 Combination with Bridging Theories
4 Basic Data Structure Theories
5 Completeness Proof
6 Conclusion
Unification and Matching in Hierarchical Combinations of Syntactic Theories
1 Introduction
2 Preliminaries
3 Hierarchical Combination
3.1 Combination Procedure for Hierarchical Combination
4 Unification in Shallow Hierarchical Combination
5 Matching in Finite Syntactic Hierarchical Combination
5.1 Mutation-Based Procedure
5.2 Combination Procedure
5.3 Example: Matching in a Theory of Distributive Exponentiation
6 Conclusion
Combining Forward and Backward Propagation
1 Introduction
2 Constraint Handling Rules
2.1 Syntax
2.2 Operational Forward Semantics
2.3 Operational Backwards Semantics
3 Combined CHR Programs
3.1 General Formulation
3.2 Forward CHR
3.3 Backward CHR
4 Interleaved Forward/Backward Propagation
5 Application for Combined Programs
5.1 Modeling
5.2 Strictly Forward
5.3 Strictly Backward
6 Conclusion
Reasoning in Large Theories
Random Forests for Premise Selection
1 Introduction
2 Premise Selection
2.1 Quality Measures
2.2 Evaluation
2.3 Used Datasets
3 Existing Algorithms
4 Adaptations to Random Forests for Premise Selection
4.1 Sample Selection
4.2 Incremental Update
4.3 Tree Size
4.4 Feature Selection
4.5 Querying a Tree
4.6 Querying a Forest
5 Experiments
6 Conclusion
Lemmatization for Stronger Reasoning in Large Theories
1 Introduction
2 Lemmatization Scenario and Initial Statistics
3 Extracting Reusable Lemmas from Refutational Proofs
3.1 Extracting Lemmas from the Natural Deduction Proofs
4 Filtering Lemmas
4.1 Additional Filters
5 Problem-Specific Premise Selection
6 Evaluation
7 Examples of New Lemmas
8 Related Work
9 Conclusion and Future Work
Author Index

Systemvoraussetzungen

Als PDF speichern Als Link merken