swMATH ID: 31982
Software Authors: Hickey, Jason J.
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.
Homepage: http://www.nuprl.org/KB/show.php?ID=453
Related Software: Cambridge LCF; Nuprl; Isabelle
Cited in: 1 Publication

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Nuprl-Light: an implementation framework for higher-order logics. Zbl 1430.68411
Hickey, Jason J.

Cited by 1 Author

1 Hickey, Jason J.

Cited in 0 Serials

Citations by Year