TY - GEN
T1 - Term-generic logic
AU - Popescu, Andrei
AU - Roşu, Grigore
PY - 2009
Y1 - 2009
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=70349335727&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=70349335727&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-03429-9_19
DO - 10.1007/978-3-642-03429-9_19
M3 - Conference contribution
AN - SCOPUS:70349335727
SN - 3642034284
SN - 9783642034282
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 290
EP - 307
BT - Recent Trends in Algebraic Development Techniques - 19th International Workshop, WADT 2008, Revised Selected Papers
T2 - 19th International Workshop on Algebraic Development Techniques, WADT 2008
Y2 - 13 June 2008 through 16 June 2008
ER -