Back to Search
Start Over
A proof theory for generic judgments
- Source :
- ACM Transactions on Computational Logic. 6:749-783
- Publication Year :
- 2005
- Publisher :
- Association for Computing Machinery (ACM), 2005.
-
Abstract
- The operational semantics of a computation system is often presented as inference rules or, equivalently, as logical theories. Specifications can be made more declarative and high level if syntactic details concerning bound variables and substitutions are encoded directly into the logic using term-level abstractions (λ-abstraction) and proof-level abstractions (eigenvariables). When one wishes to use such logical theories to support reasoning about properties of computation, the usual quantifiers and proof-level abstractions do not seem adequate: proof-level abstraction of variables with scope over sequents ( global scope) as well as over only formulas ( local scope) seem required for many examples. We will present a sequent calculus that provides this local notion of proof-level abstraction via generic judgment and a new quantifier, ∇, which explicitly manipulates such local scope. Intuitionistic logic extended with ∇ satisfies cut-elimination even when the logic is additionally strengthened with a proof theoretic notion of definitions. The resulting logic can be used to encode naturally a number of examples involving abstractions, and we illustrate the uses of ∇ with the π-calculus and an encoding of provability of an object-logic.
- Subjects :
- Discrete mathematics
Theoretical computer science
Natural deduction
General Computer Science
Logic
Sequent calculus
Intuitionistic logic
Higher-order logic
Theoretical Computer Science
Computational Mathematics
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Proof calculus
Proof theory
Structural proof theory
Rule of inference
Mathematics
Subjects
Details
- ISSN :
- 1557945X and 15293785
- Volume :
- 6
- Database :
- OpenAIRE
- Journal :
- ACM Transactions on Computational Logic
- Accession number :
- edsair.doi...........9810db508c8243c555303c4fb5038b6b