Representing scope in intuitionistic deductions

Research output: Contribution to journalReview articlepeer-review

2 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)129-188
Number of pages60
JournalTheoretical Computer Science
Volume211
Issue number1-2
DOIs
StatePublished - Jan 28 1999
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Representing scope in intuitionistic deductions'. Together they form a unique fingerprint.

Cite this