A complete system generation algorithm for list structures

Abstract

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.

Keywords:

• List structures
• LISP
• decidability
• completeness
• axiomatic systems

C.R. Categories:

• G.21
• 5.23