Frontiers of Combining Systems

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.