Frontiers of Combining Systems
8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings
Published on 1. October 2011
VIII, 275 pages
978-3-642-24364-6 (ISBN)
Description
This book constitutes the refereed proceedings of the 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011, held in Saarbrücken, Germany, in October 2011.
The 15 revised full papers presented together with three invited papers were carefully reviewed and selected from 22 submissions. The event builds a common forum for research activities in the general area of combination, modularization and integration of systems, with emphasis on logic-based ones, and of their practical use.
More details
Other editions
Additional editions
Cesare Tinelli | Viorica Sofronie-Stokkermans
Frontiers of Combining Systems
8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings
Book
09/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Invited Papers
- Tailoring Temporal Description Logics for Reasoning over Temporal Conceptual Models
- Introduction
- DL-Lite Logics
- Temporal Conceptual Modelling
- Temporal DL-Lite Logics
- Conclusions
- References
- Automatic Proof and Disproof in Isabelle/HOL
- Introduction
- Standard Proof Methods
- Simplification
- Auto and Co.
- Blast and Metis
- Sledgehammer: Proof Discovery Using External Provers
- Relevance Filtering
- Translation to First-Order Logic
- Invocation of External Provers
- Proof Reconstruction
- Proof Minimization
- Quickcheck: Counterexample Generation by Testing
- Random and Exhaustive Testing
- Test Data Generation
- Narrowing
- Nitpick: Countermodel Generation Using SAT Solvers
- Basic Translation to Relational Logic
- Approximation of Infinite Types and Partiality
- Encoding of (Co)inductive Predicates
- Encoding of (Co)inductive Datatypes
- Related Work
- Conclusion
- References
- Size-Change Termination and Satisfiability for Linear-Time Temporal Logics
- Introduction
- Linear-Time Temporal Logics
- Infinite Words
- LTL
- PSL - An Extension of LTL
- The Linear-Time µ-Calculus
- Automata on Infinite Words
- Alternating Parity Automata
- Subclasses of Alternating Parity Automata
- Constructions on Alternating Parity Automata
- Decision Problems for Alternating Parity Automata
- Alternating Parity Automata and Temporal Logics
- The Size-Change Termination Principle for Alternating Parity Automata
- Boxes and Their Composition
- Characterising the Emptiness Problem for Alternating Parity Automata
- References
- Contributed Papers
- Combining Theories: The Ackerman and Guarded Fragments
- Introduction
- Notations and Basic Definitions
- Combination of Theories
- The Guarded Fragments
- The Spectra of Guarded Fragments
- The Ackermann Class
- Conclusions
- References
- On the Undecidability of Fuzzy Description Logics with GCIs and Product T-norm
- Introduction
- T-norms and Fuzzy Logic
- Fuzzy Description Logics
- Undecidability w.r.t. Witnessed Models
- Undecidability w.r.t. Strongly Witnessed Models
- Conclusions
- References
- The Complexity of Reversal-Bounded Model-Checking
- Introduction
- Preliminaries
- From Reversal-Bounded Model-Checking to Reachability
- Complexity and Effective Presburger-Definability
- Conclusion
- References
- Expressing Polymorphic Types in a Many-Sorted Language
- Introduction
- First-Order Logic with Polymorphic Types
- Eliminating Polymorphic Types
- Symbol Discrimination
- Twin Sorts
- Decorated Terms
- Explicit Polymorphism
- Experiments and Conclusion
- References
- A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints
- Introduction
- Background and Preliminaries
- Modularized Constraints for the Theory BAXdiffIDL
- A Satisfiability Solver for BAX$_diff$ ? IDL
- Preprocessing
- Completion
- An Interpolating Solver for BAX$_diff$ ? IDL
- Interpolating Metarules
- The Interpolating Solver
- An Interpolating Solver for AX$_diff$ ? IDL
- Conclusions and Future Work
- References
- Superposition Modulo Non-linear Arithmetic
- Introduction
- Preliminaries
- SMT for Non-linear Arithmetic
- Superposition Modulo Non-linear Arithmetic
- Strong Satisfaction
- Experiments
- Conclusion
- References
- The Modal Logic of Equilibrium Models
- Introduction
- The Modal Logic of Equilibrium Models MEM
- Language
- Kripke Models
- Truth Conditions
- Axiomatics, Decidability, and Complexity
- HT Logic and Equilibrium Logic
- The Language L?
- Here-and-There Logic
- Equilibrium Logic
- From HT Logic and Equilibrium Logic to Modal Logic
- Translating L to L[T]
- From HT Logic to MEM
- From Equilibrium Logic to MEM
- Conclusion
- References
- Harnessing First Order Termination Provers Using Higher Order Dependency Pairs
- Introduction
- Preliminaries
- Splitting the System
- Simplifying the First Order Part
- Experiments
- Discussion
- References
- Stochastic Local Search for SMT: Combining Theory Solvers withWalkSAT
- Introduction
- Background
- Stochastic Local Search for SAT
- Satisfiability Modulo Theory
- Stochastic Local Search for SMT
- A Basic WalkSMT Procedure
- Enhancements to the Basic WalkSMT Procedure
- Preprocessing
- Single and Multiple Learning
- Literal Filterings
- Experimental Evaluation
- WalkSMT on SMT-LIB Instances
- WalkSMT on Random Instances
- Conclusions and Future Work
- References
- Controlled Term Rewriting
- Preliminaries
- CF and CS Tree Languages and TRS
- Controlled Term Rewriting
- Monotonic CntTRS
- Prefix Control
- Non-monotonic Rewrite Rules
- Recursive Prefix Control
- References
- Sharing Is Caring: Combination of Theories
- Introduction
- Preliminaries
- New Combination Method
- Combination Method
- Extension to Polite Combination
- Theory of Uninterpreted Functions
- Theory of Arrays
- Experimental Evaluation
- Conclusion
- References
- Modular Termination and Combinability for Superposition Modulo Counter Arithmetic
- Introduction
- A Motivating Example
- Preliminaries
- Superposition Calculus for Counter Arithmetic
- Background on Non-disjoint Combination
- Modular Termination
- A General Compatibility Result
- Applying Modular Termination and Combination
- Conclusions
- References
- Congruence Closure of Compressed Terms in Polynomial Time
- Introduction
- Preliminaries
- Term Rewriting Systems
- Grammar Compressed Terms and Term Rewriting Systems
- The Word-Problem for STG-Compressed Terms with DAG-Compressed Ground Equations
- A Normalizing Algorithm for Compressed Terms
- Deciding the Word Problem
- STG-Compressed Ground Term Rewriting Systems
- Complexity Bounds
- STG-Compressed gTRS with One Rule
- Monadic Ground Term Rewriting Systems
- Implementation and Tests
- Conclusion and Further Work
- References
- Generalized and Formalized Uncurrying
- Introduction
- Preliminaries
- Applicative Rewriting and Uncurrying
- Uncurrying in the Dependency Pair Framework
- Heuristics and Experiments
- Conclusions
- References
- A Semantic Account for Modularity in Multi-language Modelling of Search Problems
- Introduction
- Background: Model Expansion Task
- Modular Systems
- Expressive Power
- Approximating Solutions
- Related Work
- Conclusion and Future Work
- References
- Author Index
