Withdraw
Loading…
Term-Generic Logic
Popescu, Andrei; Rosu, Grigore
Loading…
Permalink
https://hdl.handle.net/2142/11513
Description
- Title
- Term-Generic Logic
- Author(s)
- Popescu, Andrei
- Rosu, Grigore
- Issue Date
- 2009-01
- Keyword(s)
- logic
- computer science
- 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.
- Type of Resource
- text
- Permalink
- http://hdl.handle.net/2142/11513
- 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
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…