Skip to main content
PRL Project

Formal Theories and Software Systems: Fundamental Connections Between Computer Science and Logic

by Robert L. Constable

In: Future Tendencies in Computer Science: Control and Applied Mathematics

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.

bibTex ref: Con92b

cite link