Description: |
Nuprl-Light: an implementation framework for higher-order logics. this paper we describe Nuprl-Light, a descendent of the Nuprl [2] theorem prover, that addresses the issues of diversity and sharing by providing a modular, object-oriented framework for specifying, relating, and developing type theories and mathematical domains. The framework itself assumes (and provides) no type theory or logic, as in LF [4], which is why we call it an implementation framework. Instead, Nuprl-Light provides a meta-framework where logical frameworks such as LF, Nuprl, set theory, and other theories can be defined and developed. Since proof automation is such a critical part of theorem proving in these logics, the implementation framework is tied closely to a programming language (in this case Caml-Light) and the formal module system is tied closely to the programming language modules. Like the Isabelle [9] generic theorem prover, Nuprl-Light uses generalized Horn clauses for logical specification. Indeed, specifications in Nuprl-Light appear quite similar to those in Isabelle. However, where Isabelle uses higher order unification and resolution, Nuprl-Light retains a tactic–tree [3] of LCF [8] style reasoning based on tactics and tacticals, and Nuprl-Light also allows theories to contain specifications of rewrites, using the computational congruence of Howe [7]. Like LF, the Nuprl-Light meta-logic also relies on the judgments–as– types principle (an extension of propositions–as–type), where proofs are terms that inhabit the clauses. |