This book constitutes the refereed proceedings of the 5th International Workshop on Frontiers of Combining Systems, FroCoS 2005, held in Vienna, Austria, in September 2005.
The 19 revised full papers presented including 2 system descriptions were carefully reviewed and selected from 28 submissions. The papers are organized in topical sections on combinations of logics, theories, and decision procedures; constraint solving and programming; combination issues in rewriting and programming as well as in logical frameworks and theorem proving systems.
Author(s): Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli (auth.), Bernhard Gramlich (eds.)
Series: Lecture Notes in Computer Science 3717 : Lecture Notes in Artificial Intelligence
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2005
Language: English
Pages: 321
Tags: Artificial Intelligence (incl. Robotics); Mathematical Logic and Formal Languages; Programming Techniques; Software Engineering
Front Matter....Pages -
A Comprehensive Framework for Combined Decision Procedures....Pages 1-30
Connecting Many-Sorted Structures and Theories Through Adjoint Functions....Pages 31-47
Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic....Pages 48-64
On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal....Pages 65-80
Sociable Interfaces....Pages 81-105
About the Combination of Trees and Rational Numbers in a Complete First-Order Theory....Pages 106-121
A Complete Temporal and Spatial Logic for Distributed Systems....Pages 122-137
Hybrid CSP Solving....Pages 138-167
An Efficient Decision Procedure for UTVPI Constraints....Pages 168-183
Declarative Constraint Programming with Definitional Trees....Pages 184-199
Logical Analysis of Hash Functions....Pages 200-215
Proving and Disproving Termination of Higher-Order Functions....Pages 216-231
Proving Liveness with Fairness Using Rewriting....Pages 232-247
A Concurrent Lambda Calculus with Futures....Pages 248-263
The ASM Method for System Design and Analysis. A Tutorial Introduction....Pages 264-283
Matching Classifications via a Bidirectional Integration of SAT and Linguistic Resources....Pages 284-284
Connecting a Logical Framework to a First-Order Logic Prover....Pages 285-301
Combination of Isabelle/HOL with Automatic Tools....Pages 302-309
ATS: A Language That Combines Programming with Theorem Proving....Pages 310-320
Back Matter....Pages -
