Loading...
Please wait, while we are loading the content...
Similar Documents
Formalising a model of the lambda-calculus in hol-st (1994).
| Content Provider | CiteSeerX |
|---|---|
| Author | Agerholm, Sten |
| Abstract | Most new theorem provers implement strong and complicated type theories which eliminate some of the limitations of simple type theories such as the HOL logic. A more accessible alternative might be to use a combination of set theory and simple type theory as in HOL-ST which is a version of the HOL system supporting a ZF-like set theory in addition to higher order logic. This paper presents a case study on the use of HOL-ST to build a model of the -calculus by formalising the inverse limit construction of domain theory. This construction is not possible in the HOL system itself, or in simple type theories in general. 1 Introduction The HOL system [GM93] supports a simple and accessible yet very powerful logic, called higher order logic or simple type theory. This is probably a main reason why it has one of the largest user communities of any theorem prover today. However, it is heard every now and then that users cannot quite do what they would like to do, e.g. due to restrictions in t... |
| File Format | |
| Publisher Date | 1994-01-01 |
| Access Restriction | Open |
| Subject Keyword | Simple Type Theory Hol System Powerful Logic User Community Hol Logic Case Study Set Theory Domain Theory New Theorem Provers Type Theory Order Logic Theorem Prover Today Zf-like Set Theory Inverse Limit Construction Main Reason Hol System Gm93 |
| Content Type | Text |
| Resource Type | Article |
