Dagstuhl Seminar on Semantic Foundations of Proof-search

1-6 April 2001.

David Pym, Eike Ritter and Thomas Streicher

9.30h-10.30h	David Pym Semantic Foundations of Proof search
11.00h-12.00h	Conor McBride Elimination with a Motive
14.00h-15.00h	Kurt Ranalter A decision procedure and Kripke-style semantics for the language ILP of Intuitionistic Formal Pragmatics
15.00h-15.45h	Andrea Schalk Games played on Graphs
16.15h-17.00h	Dominique Larchey-Wendling Refutation as Counter-Models for Intuitionistic Logic
17.00h-17.30h	Roy Dyckhoff Rule invertibility in Sequent Calculi

Tuesday, 3 April

9.30h-10.30h	Eike Ritter Modelling Backtracking
11.00h-12.00h	Didier Galmiche Proof Search and Counter-Model Generation in Mixed Logics
14.00h-15.00h	Edmund Robinson Proof Nets for Classical Logic
15.00h-15.30h	Alberto Momigliano A " Negative " Look to Uniform Proof Search
15.30h-16.00h	Uwe Egly A Polynomial Translation of Propositional S4 into Propositional Intuitionistic Logic
16.30h-17.15h	Gianluigi Bellin Towards a Formal Pragmatics

Wednesday, 4 April

9.30h-10.30h	Andrei Voronkov Syntactic Foundations of Proof Search
11.00h-11.45h	Iliano Cervesato A Linear Spine Calculus
11.45h-12.15h	James McKinna Towards a Calculus of Problems in Type Theory with Applications to Relational Rippling

Thursday, 5 April

9.00h-9.45h	Jim Lipton Semantics of Higher-order Logic Programming
9.45h-10.45h	Patricia Hill Logic Programming, Data-Flow Analysis and Equality Theories
11.00h-11.30h	Robert Staerk Problems of Bytecode Verification
11.30h-12.00h	Thomas Streicher Ontological Status of Paraproofs
14.00h-14.30h	Kevin Watkins Defining An Operational Semantics for Resource Management in Lolli
14.30h-15.00h	Alan Smaill A Research Specification Language in Practice
15.00h-15.30h	Randy Pollack On the Extensibility of Proof Checkers
15.30h-16.00h	Konstantin Korovin Solving Knuth-Bendix Ordering Constraints

Friday, 6 April

9.30h-10.00h	Manfred Kerber Towards a Classification of Proofs
10.00h-10.30h	Alexandre Riazanov Splitting without backtracking
11.00h-11.30h	Roy Dyckhoff Proof Search and Computation in Herbelin's calculus