Frontiers of Combining Systems: Third International Workshop, FroCoS 2000 Nancy, France, March 22-24, 2000 Proceedings (Lecture Notes in Computer Science, 1794)

This book constitutes the refereed proceedings of the Third International Workshop on Frontiers of Combining Systems, FroCoS 2000, held in Nancy, France, in March 2000. The 14 revised full papers presented together with four invited papers were carefully reviewed and selected from a total of 31 submissions. Among the topics covered are constraint processing, interval narrowing, rewriting systems, proof planning, sequent calculus, type systems, model checking, theorem proving, declarative programming, logic programming, and equational theories. 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. Invited Paper -- Combining Logic And Optimization In Cutting Plane Theory -- Session 1 -- Towards Cooperative Interval Narrowing -- Integrating Constraint Solving Into Proof Planning -- Termination Of Constraint Contextual Rewriting -- Invited Paper -- Axioms Vs. Rewrite Rules: From Completeness To Cut Elimination -- Session 2 -- Normal Forms And Proofs In Combined Modal And Temporal Logics -- Structured Sequent Calculi For Combining Intuitionistic And Classical First-order Logic -- Session 3 -- Handling Differential Equations With Constraints For Decision Support -- Non-trivial Symbolic Computations In Proof Planning -- Integrating Computer Algebra And Reasoning Through The Type System Of Aldor -- Invited Paper -- Combinations Of Model Checking And Theorem Proving -- Session 4 -- Compiling Multi-paradigm Declarative Programs Into Prolog -- Modular Redundancy For Theorem Proving -- Composing And Controlling Search In Reasoning Theories Using Mappings -- Invited Paper -- Why Combined Decision Problems Are Often Intractable -- Session 5 -- Congruence Closure Modulo Associativity And Commutativity -- Combining Equational Theories Sharing Non-collapse-free Constructors -- Comparing Expressiveness Of Set Constructor Symbols. [edited By] Hélène Kirchner, Christophe Ringeissen. Includes Bibliographical References And Index. Front Matter....Pages - Combining Logic and Optimization in Cutting Plane Theory....Pages 1-17 Towards Cooperative Interval Narrowing....Pages 18-31 Integrating Constraint Solving into Proof Planning....Pages 32-46 Termination of Constraint Contextual Rewriting....Pages 47-61 Axioms vs. Rewrite Rules: From Completeness to Cut Elimination....Pages 62-72 Normal Forms and Proofs in Combined Modal and Temporal Logics....Pages 73-87 Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic....Pages 88-104 Handling Differential Equations with Constraints for Decision Support....Pages 105-120 Non-trivial Symbolic Computations in Proof Planning....Pages 121-135 Integrating Computer Algebra and Reasoning through the Type System of Aldor....Pages 136-150 Combinations of Model Checking and Theorem Proving....Pages 151-170 Compiling Multi-paradigm Declarative Programs into Prolog....Pages 171-185 Modular Redundancy for Theorem Proving....Pages 186-199 Composing and Controlling Search in Reasoning Theories Using Mappings....Pages 200-216 Why Combined Decision Problems Are Often Intractable....Pages 217-244 Congruence Closure Modulo Associativity and Commutativity....Pages 245-259 Combining Equational Theories Sharing Non-Collapse-Free Constructors....Pages 260-274 Comparing Expressiveness of Set Constructor Symbols....Pages 275-289 Back Matter....Pages - Frontiers of Combining Systems: Third International Workshop, FroCoS 2000, Nancy, France, March 22-24, 2000. Proceedings Author: Hélène Kirchner, Christophe Ringeissen Published by Springer Berlin Heidelberg ISBN: 978-3-540-67281-4 DOI: 10.1007/10720084 Table of Contents: Combining Logic and Optimization in Cutting Plane Theory Towards Cooperative Interval Narrowing Integrating Constraint Solving into Proof Planning Termination of Constraint Contextual Rewriting Axioms vs. Rewrite Rules: From Completeness to Cut Elimination Normal Forms and Proofs in Combined Modal and Temporal Logics Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic Handling Differential Equations with Constraints for Decision Support Non-trivial Symbolic Computations in Proof Planning Integrating Computer Algebra and Reasoning through the Type System of Aldor Combinations of Model Checking and Theorem Proving Compiling Multi-paradigm Declarative Programs into Prolog Modular Redundancy for Theorem Proving Composing and Controlling Search in Reasoning Theories Using Mappings Why Combined Decision Problems Are Often Intractable Congruence Closure Modulo Associativity and Commutativity Combining Equational Theories Sharing Non-Collapse-Free Constructors Comparing Expressiveness of Set Constructor Symbols This book constitutes the refereed proceedings of the 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013, held in Nancy, France, in September 2013. The 20 revised full papers presented together with 4 invited papers were carefully reviewed and selected from 33 submissions. FroCoS'13 seeks to offer a common forum for research in the general area of combination,modularization and integration of systems, with emphasis on logic-based ones, and of their practical use. Typical topics of interest include following subjects: combinations of logics such as combined predicate, temporal, modal or epistemic logics, combinations and modularity in ontologies, combination of decision, procedures, of satisfiability, procedures and of constraint solving techniques, combinations and modularity in term rewriting, integration of equational and other theories into deductive systems, combination of deduction systems and computer algebra, integration of data structures into constraint logic programming and deduction, and modularizing programs and specifications. Cutting planes were introduced in a seminal paper of Gomory (1958) in order to solve linear optimization problems over the integer numbers.