Nuprl-Light: an implementation framework for higher-order logics. this paper we describe Nuprl-Light, a descendent of the Nuprl  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 , 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  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  of LCF  style reasoning based on tactics and tacticals, and Nuprl-Light also allows theories to contain specifications of rewrites, using the computational congruence of Howe . 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.
References in zbMATH (referenced in 1 article , 1 standard article )
Showing result 1 of 1.