Computation of Full Logic Programs Using One-Variable Environments

Computation of formulas of the full first order predicate calculus is performed by first converting the multi-variable formulas into a single variable presentation of the Theory of Pairs (TP). Pairs are symbolic expressions of LISP with only one atom 0. Single variable calculus is suitable for both computations and mechanical theorem proving because the problems of multiple variable names and clashes between free and bound variables are eliminated. We present a logic programming language R⁺-Maple which computes by solving equations instead of unifications and refutations. Pairs permit a single one-variable equation called environment equation to hold the values or all variables. Traditionally environments are implementation tools used to carry bindings or variables during the computation. With the help of environment equations for the single variable of our calculus we make the environments visible within the framework of a first order theory. This allows a straightforward demonstration of soundness of our computations. Moreover, the explicit form of environments allows to experiment with different forms of computational rules directly within the logic. The soundness of new rules can be thus readily proven formally. This has the advantage over the traditional method which buries the rules, as they are closely connected with environments, deeply within the code of an interpreter.