University of Illinois Urbana-Champaign

Term-Generic First-Order Logic

Papescu, Andrei; Rosu, Grigore

Content Files
Term-Generic First-Order Logic.pdf

Permalink

https://hdl.handle.net/2142/11196

Description

Title
Term-Generic First-Order Logic
Author(s)
  • Papescu, Andrei
  • Rosu, Grigore
Issue Date
2006-04
Keyword(s)
computer science
Date of Ingest
2009-04-21T14:41:39Z
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.
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11196
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY