Transformers for Symbolic Computation and Formal Deduction

William M. Farmer and Martin v. Mohrenschildt

2000

Abstract

A transformer is a function that maps expressions to expressions.
Many transformational operators -- such as expression evaluators and
simplifiers, 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 defining sound transformers in the
context of an axiomatic theory in a formal logic.  The paper is
intended to be a first step in a development of an integrated
framework for symbolic computation and formal deduction.