Files in this item



application/pdfTerm-Generic First-Order Logic.pdf (461kB)
(no description provided)PDF


Title:Term-Generic First-Order Logic
Author(s):Papescu, Andrei; Rosu, Grigore
Subject(s):computer science
Abstract:Term-generic first-order logic, or simply generic first-order logic (GFOL), is presented as 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. A complete Gentzen deduction system is given, as well as complete equational and many-sorted extensions. It is shown that various calculi with binding, such as lambda-calculus and System F, can be faithfully defined as GFOL theories. Since GFOL is complete, by defining a logic or calculus as a GFOL theory one gets, at no additional effort, a semantics for that logic or calculus. A fragment of GFOL called Horn^2 is also defined, on whose theories, under certain conditions, the generic Gentzen deduction system is equivalent to a simplified deduction system which resembles the derivation system of the calculi that we intend to explicitly capture. Consequently, GFOL and especially its fragment Horn^2 can serve as a foundationaldefinitional framework for other calculi and logics, providing these with models and complete deduction.
Issue Date:2006-04
Genre:Technical Report
Other Identifier(s):UIUCDCS-R-2006-2717
Date Available in IDEALS:2009-04-21

This item appears in the following Collection(s)

Item Statistics