Importing Isabelle Formal Mathematics into NuPRL

by Pavel Naumov
1998-1999

Isabelle is a generic higher order theorem prover designed to support different axiomatic theories. A general idea how such theories can be interpreted in NuPRL was described in my September presentation on PRL Seminar:

This time, after a brief summary of the last year presentation, I will talk about Howe-style automated converter from Isabelle into NuPRL that I have developed and about logical foundations behind this converter. Unlike D. Howe, who gives semantical justification of his interpretation of HOL in Isabelle, I provide a direct syntactical proof.

In the last part of the presentation, current work-in-progress on formalization of this proof in NuPRL will be discussed.

Importing Isabelle Formal Mathematics into NuPRL

by Pavel Naumov 1998-1999

by Pavel Naumov
1998-1999