A complete system generation algorithm for list structures
Richard Butrick · International Journal of Computer Mathematics · 1986
Previous axiomatic studies of the list structures of LISP by Moore and by Butrick have pointed out that the full system for list structures with recursion and an induction schema is incomplete(able). This paper develops a decision procedure for elementary list structures without recursion (List-S) which is complete. Every sentence of List-S is shown to be such that either it or its negation is a member (theorem) of List-S by the decision procedure.