Frontiers of Combining Systems

Name: Frontiers of Combining Systems | 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings

Cesare Tinelli Viorica Sofronie-Stokkermans(Herausgeber*in)

Springer (Verlag)

Erschienen am 1. Oktober 2011

VIII, 275 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-24364-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
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

Systemvoraussetzungen

Als PDF speichern Als Link merken