Dagstuhl Seminar on Semantic Foundations of Proof-search
1-6 April 2001.

David Pym, Eike Ritter and Thomas Streicher


Programme



Monday, 2 April


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