Frontiers of Combining Systems: Third International Workshop, FroCoS 2000 Nancy, France, March 22-24, 2000 Proceedings

Front Cover
Springer Science & Business Media, Mar 15, 2000 - Computers - 289 pages
This volume contains the proceedings of FroCoS2000, the 3rd International WorkshoponFrontiersofCombiningSystems, heldMarch22-24,2000, inNancy, France. Like its predecessors organized in Munich (1996) and in Amsterdam (1998), FroCoS2000 is intended to o?er a common forum for research activities related to the combination and the integration of systems in the areas of logic, automateddeduction, constraintsolving, declarativeprogramming, andarti?cial intelligence. There were 31 submissions of overall high quality, authored by researchers from countries including Australia, Brasil, Belgium, Chili, France, Germany, - pan, Ireland, Italy, Portugal, Spain, Switzerland, The Netherlands, the United Kingdom, and the United States of America. All submissions were thoroughly evaluatedonthebasisofatleastthreerefereereports, andanelectronicprogram committeemeetingwasheldthroughtheInternet.Theprogramcommitteesel- ted 14 research contributions. The topics covered by the selected papers include: combinationoflogics;combinationofconstraintsolvingtechniques, combination of decision procedures; modular properties for theorem proving; combination of deduction systems and computer algebra; integration of decision procedures and other solving processes into constraint programming and deduction systems. We welcomed ?ve invited lectures by Alexander Bockmayr on "Combining Logic and Optimization in Cutting Plane Theory," Gilles Dowek on "Axioms vs. Rewrite Rules: From Completeness to Cut Elimination," Klaus Schulz on "Why Combined Decision Problems Are Often Intractable," Tomas Uribe on "Combinations of Theorem Proving and Model Checking," and Richard Zippel on "Program Composition Techniques for Numerical PDE Codes." Full papers of these lectures, except the last one, are also included in this volume.
 

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Combining Logic and Optimization in Cutting Plane Theory
1
Towards Cooperative Interval Narrowing
18
Integrating Constraint Solving into Proof Planning
32
Termination of Constraint Contextual Rewriting
47
From Completeness to Cut Elimination
62
Normal Forms and Proofs in Combined Modal and Temporal Logics
73
Structured Sequent Calculi for Combining Intuitionistic and Classical FirstOrder Logic
88
Handling Differential Equations with Constraints for Decision Support
105
Combinations of Model Checking and Theorem Proving
151
Compiling Multiparadigm Declarative Programs into Prolog
171
Modular Redundancy for Theorem Proving
186
Composing and Controlling Search in Reasoning Theories Using Mappings
200
Why Combined Decision Problems Are Often Intractable
217
Congruence Closure Modulo Associativity and Commutativity
245
Combining Equational Theories Sharing NonCollapseFree Constructors
260
Comparing Expressiveness of Set Constructor Symbols
275

Nontrivial Symbolic Computations in Proof Planning
121
Integrating Computer Algebra and Reasoning through the Type System of Aldor
136

Other editions - View all

Common terms and phrases