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(Editor)

Springer (Publisher)

Published on 19. September 2015

XVII, 357 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-24246-0 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Persons

Content

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

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Frontiers of Combining Systems

Description

More details

Other editions

Additional editions

Persons

Content

System requirements