Nuprl-Light 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 Document Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Nuprl-Light: an implementation framework for higher-order logics. Zbl 1430.68411Hickey, Jason J. 1997 Cited by 1 Author 1 Hickey, Jason J. Cited in 0 Serials Cited in 2 Fields 1 Mathematical logic and foundations (03-XX) 1 Computer science (68-XX) Citations by Year