Term-generic logic

Andrei Popescu, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 λ-calculi. Horn 2 appears to be sufficient for defining a whole plethora of λ-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.

Original languageEnglish (US)
Title of host publicationRecent Trends in Algebraic Development Techniques - 19th International Workshop, WADT 2008, Revised Selected Papers
Number of pages18
StatePublished - 2009
Event19th International Workshop on Algebraic Development Techniques, WADT 2008 - Pisa, Italy
Duration: Jun 13 2008Jun 16 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5486 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other19th International Workshop on Algebraic Development Techniques, WADT 2008

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Term-generic logic'. Together they form a unique fingerprint.

Cite this