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