FroCoS'2000 Program

Frontiers of Combining Systems

March 22-24, 2000

Nancy, France

CONSEIL GENERAL de MEURTHE et MOSELLE

48, rue du Sergent Blandan

Wednesday, March 22

09:00-09:30, Welcome and Introduction

Hélène Kirchner and Christophe Ringeissen

09:30-10:30, Invited Talk

Alexander Bockmayr (LORIA, Nancy):
Combining Logic and Optimization in Cutting Plane Theory

Break

11:00-12:30, Session 1

11:00	Towards Cooperative Interval Narrowing
	L.Granvilliers
11:30	Constraint Solving in Proof Planning
	E.Melis, J.Zimmer, T.Mueller
12:00	Termination of Constraint Contextual Rewriting
	A.Armando, S.Ranise

Lunch

14:00-15:00, Invited Talk

Gilles Dowek (INRIA-Rocquencourt):
Axioms vs. rewrite rules: from completeness to cut elimination

Break

15:30-16:30, Session 2

15:30	Normal Forms and Proofs in Combined Modal and Temporal Logics
	U.Hustadt, C.Dixon, R.A.Schmidt, M.Fisher
16:00	Structured Sequent Calculi for Combining Intuitionistic and Classical First-Order Logic
	P.Lucio

Visit of Nancy and Conference Dinner

09:00-10:00, Invited Talk

Nachum Dershowitz (Tel Aviv University):
Combined Rewriting

Break

10:30-12:00, Session 3

10:30	Handling Differential Equations with Constraints for Decision Support
	J.Cruz, P.Barahona
11:00	Non-trivial Computations in Proof Planning
	V.Sorge
11:30	Integrating computer algebra and reasoning through the type system of Aldor
	E.Poll, S.Thompson

Lunch

13:30-14:30, Invited Talk

Tomas Uribe (Stanford University):
Combinations of Model Checking and Theorem Proving

Break

15:00-16:30, Session 4

15:00	Compiling Multi-Paradigm Declarative Programs into Prolog
	S.Antoy, M.Hanus
15:30	Modular Redundancy for Theorem Proving
	M.Bofill, G.Godoy, R.Nieuwenhuis, A.Rubio
16:00	Composing and Controlling Search in Reasoning Theories using Mappings
	A.Coglio, F.Giunchiglia, J.Meseguer, C.Talcott

Visit of Musée de l'Ecole de Nancy and Reception at Conseil Général

09:00-10:00, Invited Talk

Klaus Schulz (LMU Muenchen):
Why combined decision problems are often intractable

Break

10:30-12:00, Session 5

10:30	Congruence Closure Modulo Associativity-Commutativity
	L.Bachmair, I.V.Ramakrishnan, A.Tiwari, L.Vigneron
11:00	Combining Equational Theories Sharing Non-Collapse-Free Constructors
	F.Baader, C.Tinelli
11:30	Comparing expressiveness of set constructor symbols
	A.Dovier, C.Piazza, A.Policriti

12:00-12:30, Business Meeting

Lunch

End of the Conference