Search

MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project involving several universities in several countries. The MetaPRL system combines the properties of an interactive LCF-style tactic-based proof assistant, a logical framework, a logical programming environment, and a formal methods programming toolkit. MetaPRL is distributed under an open-source license and can be downloaded from http://metaprl.org/. This paper provides an overview of the system focusing on the features that did not exist in the previous generations of PRL systems. [ABSTRACT FROM AUTHOR]

The Nuprl system is a framework for reasoning about mathematics and programming. Over the years its design has been substantially improved to meet the demands of large-scale applications. Nuprl LPE, the newest release, features an open, distributed architecture centered around a flexible knowledge base and supports the cooperation of independent formal tools. This paper gives a brief overview of the system and the objectives that are addressed by its new architecture. [ABSTRACT FROM AUTHOR]

A formal Theory of Logics is sketched using concepts from a modern proof development system (like Nuprl, Coq or other such software systems). The Theory can be applied to understanding these software systems, and the application suggests a design principle called the theories-as-systems notion. Applications of the Theory to automated reasoning have led to an empirical study of the notion of obvious inference. Experimental results are cited to explain key constants of a scientific theory of obvious inference. The constants appear in what is called here the deBruijn equation. [ABSTRACT FROM AUTHOR]