April 1 – 6 , 2001, Dagstuhl Seminar 01141

Semantic Foundations of Proof-search


David J. Pym (University of Bath, GB)
Eike Ritter (University of Birmingham, GB)
Thomas Streicher (TU Darmstadt, DE)

For support, please contact

Dagstuhl Service Team


List of Participants
Dagstuhl's Impact: Documents available
Dagstuhl-Seminar-Report 303


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.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.