Transformers for Symbolic Computation and Formal Deduction
William M. Farmer · 2000
. A transformer is a function that maps expressions to expressions. Many transformational operators|such as expression evaluators and simpliers, rewrite rules, rules of inference, and decision procedures|can be represented by transformers. Computations and deductions can be formed by applying sound transformers in sequence. This paper introduces machinery for dening sound transformers in the context of an axiomatic theory in a formal logic. The paper is intended to be a rst step in a development of an integrated framework for symbolic computation and formal deduction. 1 Introduction Mechanized mathematics is the study of how the computer can be used to support, improve, and automate the mathematical reasoning process. The eld is divided into two quite separated camps: computer algebra and theorem proving. Computer algebra focuses on nonbranching symbolic computations over concrete structures implemented by fast, but not necessarily, sound algorithms. Theorem proving focus...