(Bath)

Since its earliest conception, (proof theory in) mathematical logic has been formulated as a formalization of deductive reasoning: given a collection of hypotheses, a conclusion is derived. The advent of computational logic, however, has emphasized the significance of reductive reasoning: given a putative conclusion, sufficient hypotheses are determined. We provide, for intuitionistic logic and classical logic, a model-theoretic semantics of reductions of comparable value to those available for proofs. Within this general theory, which combines BHK and Kripke semantics, we formulate a model-theoretic semantics for proof-search, giving a specific games model interpretation of the key control mechanism known as backtracking.Robert Recorde Room

Department of Computer Science