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

## by Robert L. Constable

1992

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

**Abstract**

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