Sciweavers

ENTCS
2007

A Logic for Reasoning about Generic Judgments

13 years 3 months ago
A Logic for Reasoning about Generic Judgments
This paper presents an extension of a proof system for encoding generic judgments, the logic FOλ∆ of Miller and Tiu, with an induction principle. The logic FOλ∆ is itself an extension of intuitionistic logic with fixed points and a “generic quantifier”, , which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλ∆ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on , in particular by adding the axiom B ≡ x.B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated.
Alwen Tiu
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Alwen Tiu
Comments (0)