Term-Generic Logic

From FSL
Revision as of 16:58, 18 February 2015 by Grosu (Talk | contribs)

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search


J. of TCS

Term-Generic Logic
Andrei Popescu and Grigore Rosu
Journal of Theoretical Computer Science, Volume 577(1), pp 1-24. 2015
Abstract. We introduce term-generic logic (TGL), a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring terms to only provide free variable and substitution operators satisfying some reasonable axioms. TGL has a notion of model that generalizes both first-order models and Henkin models of the lambda-calculus. The abstract notions of term syntax and model are shown to be sufficient for obtaining the completeness theorem of a Gentzen system generalizing that of first-order logic. Various systems featuring bindings and contextual reasoning, ranging from pure type systems to the pi-calculus, are captured as theories inside TGL. For two particular, but rather typical instances---untyped lambda-calculus and System F---the general-purpose TGL models are shown to be equivalent with standard ad hoc models.
PDF, project, DOI, Journal of Theoretical Computer Science, BIB



WADT'08

Andrei Popescu and Grigore Rosu
WADT'08, LNCS 5486, pp 290-307. 2009
Abstract. Term-generic logic (TGL) is a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. TGL has a complete Gentzen system generalizing that of first-order logic. A certain fragment of TGL, called Horn^2, possesses a much simpler Gentzen system, similar to traditional typing derivation systems of lambda-calculi. Horn^2 appears to be sufficient for defining a whole plethora of lambda-calculi as theories inside the logic. Within intuitionistic TGL, a Horn^2 specification of a calculus is likely to be adequate by default. A bit of extra effort shows adequacy w.r.t. classic TGL as well, endowing the calculus with a complete loose semantics.
LNCS, WADT'08, BIB

Personal tools
Namespaces

Variants
Actions
Navigation