Open Architecture for Formal Reasoning
John McCarthy · 1991
This task represents an initial part of a long term project aimed at making both theoretical and practical advances in the field of formal reasoning. The main goal is to provide a framework for designing and experimenting with symbol manipulation programs, and in particular, to provide a general software architecture for implementing formal reasoning systems and interfaces to existing software components including special purpose theorem provers, program transformers, and databases. The kernel will be a computation system that supports a rich collection of data structures for formal reasoning, a wide spectrum of programming paradigms including both high-level constructs, and objects as self contained entities that may be used uniformly and independently of internal representation.