Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #544 | |
|---|---|
| Title: | Experience with Fso as a Framework Theory |
| Authors: | Matthews,S; Smaill,AD; Basin,D |
| Date: | 1991 |
| Presented: | Informal Proceedings of the 2nd "Logical Frameworks" Basic Research Action Workshop (LFBRA) 1991. |
| Keywords: | |
| Abstract: | Feferman has proposed a logic, FSo, as an alternative system for encoding logics and also for reasoning about those encodings. We have implemented a version of this system and performed experiments that show that his system is practical. Specifically, we describe a formalization of predicate calculus and the development of an admissible rule that manipulates formulas with bound variables. This application will be of interest to researchers working with frameworks that use mechanisms such as substitution in the lambda calculus to implement variable binding and substitution in the declared logic directly. We suggest that formalizing, and reasoning about, bound variables is not as difficult as is often supposed, and leads to a more powerful theory about the encoded logic. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}