Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 01141

Semantic Foundations of Proof-search

( Apr 01 – Apr 06, 2001 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



Traditionally, logics are formulated as systems of deductive inference in which proofs are constructions which derive conclusions from given assumptions. However, in computing, many problems are naturally formulated as questions of reductive inference in which the correctness of a given putative conclusion must be shown by reduction, commonly formulated as proof-search in a given formal system, to established acceptable assumptions. Examples of this phenomenon include type-inference, parsing, program correctness and internet information retrieval. Typically, such examples are described as long and complex formal texts. Consequently, algorithmic proof-search is a fundamental enabling technology throughout the computing sciences. Moreover, the reductive view of inference represents an alternative view of logic, just as fundamental as the deductive one, which is largely undeveloped.

So far, the theory of proof-search has developed mostly along proof-theoretic lines but using many type-theoretic techniques. The utility of type-theoretic methods suggests that semantic methods of the kind found to be valuable in the semantics of programming languages should be useful in tackling the main outstanding difficulty in the theory of proof-search, i.e., the representation of intermediate stages in the search for a proof. The space of searches is much larger than the space of proofs: An adequate semantics would represent both the space of searches and the space of proofs and give an account of the recovery of proofs (which are extensional objects) from searches (which are more intensional objects). It would distinguish between different proof-search strategies and permit analyses of their relative merits.

This seminar helps to establish a program to build such a semantics. To this end, we propose the following foci for the seminar:

  • Reductive vs. deductive logic: their logical, mathematical and computational properties;
  • Proof-search in type-theoretic languages: the role of typing constraints during proof-search;
  • Proof- and model-theoretic analyses of search spaces: the search-oriented counterparts to traditional proof theory and model theory;
  • Intensional semantics for proof-search: specific intensional and computational models based on structures such as games, continuations and realizability;
  • Applications of proof-theoretic and semantic techniques to the design and implementation of theorem provers.

  • Gianluigi Bellin (University of Verona, IT)
  • Iliano Cervesato (ITT Inc. - Alexandria, US) [dblp]
  • Ewen W. Denney (University of Edinburgh, GB) [dblp]
  • Roy Dyckhoff (University of St. Andrews, GB)
  • Uwe Egly (TU Wien, AT) [dblp]
  • Didier Galmiche (LORIA - Nancy, FR)
  • Patricia Hill (University of Leeds, GB)
  • Manfred Kerber (University of Birmingham, GB)
  • Konstantin Korovin (University of Manchester, GB) [dblp]
  • Dominique Larchey-Wendling (LORIA - Nancy, FR) [dblp]
  • Jim Lipton (Wesleyan Univ. - Middletown, US)
  • Conor McBride (Durham University, GB) [dblp]
  • James McKinna (University of St. Andrews, GB) [dblp]
  • Daniel Mery (CNRS - Nancy, FR)
  • Alberto Momigliano (University of Leicester, GB) [dblp]
  • Michel Parigot (University Paris-Diderot, FR)
  • Randy Pollack (University of Edinburgh, GB)
  • David J. Pym (University of Bath, GB) [dblp]
  • Kurt Ranalter (University of Verona, IT)
  • Alexandre Riazanov (University of Manchester, GB)
  • Eike Ritter (University of Birmingham, GB)
  • Edmund Robinson (Queen Mary University of London, GB)
  • Andrea Schalk (University of Manchester, GB)
  • Alan Smaill (University of Edinburgh, GB) [dblp]
  • Robert Stärk (ETH Zürich, CH)
  • Thomas Streicher (TU Darmstadt, DE)
  • Hayo Thielecke (University of Birmingham, GB)
  • Andrei Voronkov (University of Manchester, GB) [dblp]
  • Kevin Watkins (Carnegie Mellon University - Pittsburgh, US)