TY - JOUR

T1 - Representing scope in intuitionistic deductions

AU - Stone, Matthew

N1 - Funding Information:
NSF graduate fellowship, and an IRCS graduate fellowship, as well as NSF grant IRI95-04372, ARPA grant N6601-94-C6043, and AR0 grant DAAH05-94-G0426.

PY - 1999/1/28

Y1 - 1999/1/28

N2 - Intuitionistic proofs can be segmented into scopes which describe when assumptions can be used. In standard descriptions of intuitionistic logic, these scopes occupy contiguous regions of proofs. This leads to an explosion in the search space for automated deduction, because of the difficulty of planning to apply a rule inside a particular scoped region of the proof. This paper investigates an alternative representation which assigns scope explicitly to formulas, and which is inspired in part by semantics-based translation methods for modal deduction. This calculus is simple and is justified by direct proof-theoretic arguments that transform proofs in the calculus so that scopes match standard descriptions. A Herbrand theorem, established straightforwardly, lifts this calculus to incorporate unification. The resulting system has no impermutabilities whatsoever - rules of inference may be used equivalently anywhere in the proof. Nevertheless, a natural specification describes how λ-terms are to be extracted from its deductions.

AB - Intuitionistic proofs can be segmented into scopes which describe when assumptions can be used. In standard descriptions of intuitionistic logic, these scopes occupy contiguous regions of proofs. This leads to an explosion in the search space for automated deduction, because of the difficulty of planning to apply a rule inside a particular scoped region of the proof. This paper investigates an alternative representation which assigns scope explicitly to formulas, and which is inspired in part by semantics-based translation methods for modal deduction. This calculus is simple and is justified by direct proof-theoretic arguments that transform proofs in the calculus so that scopes match standard descriptions. A Herbrand theorem, established straightforwardly, lifts this calculus to incorporate unification. The resulting system has no impermutabilities whatsoever - rules of inference may be used equivalently anywhere in the proof. Nevertheless, a natural specification describes how λ-terms are to be extracted from its deductions.

UR - http://www.scopus.com/inward/record.url?scp=0007887778&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0007887778&partnerID=8YFLogxK

U2 - 10.1016/S0304-3975(98)00244-8

DO - 10.1016/S0304-3975(98)00244-8

M3 - Review article

AN - SCOPUS:0007887778

VL - 211

SP - 129

EP - 188

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-2

ER -