By the late 1970's, computing had changed in fundamental ways, and it was felt that the theorem-proving effort would benefit from a complete redesign of the system that would make it more robust. For one thing, the rise of the science of software engineering had contributed new knowledge about how to structure large systems. For another, portability and ease of use were becoming standard requirements for software, and the Argonne-NIU group wanted to be able to share their prover with other researchers in the area. Thirdly, computer systems were becoming more interactive.
Lusk and Overbeek decided to re-implement the system from scratch, with an eye to all of these concerns. A layered library approach was chosen, with Pascal as the implementation language. (A strange choice, perhaps, but one needs to recall that at that time, Lisp was not yet fast, C was not yet public, and Ada looked promising as a new standard portable language that would include multiprocessing facilities. Lusk and Overbeek thought that they would probably eventually translate the system into Ada, and the syntactically similar Pascal would make it easier to do this automatically.)
The new system, written by Lusk, McCune, and Overbeek, was called LMA (Logic Machine Architecture) and had three distinct layers. The lowest layer[8] supplied a set of objects that eliminated the limits that had been encountered in extending the NIUTP systems into new domains. LMA would have no built-in limits on the number of arguments per term or literals per clause. The first layer also supplied indexing and unification services. The second layer[7] supplied the inference rules and demodulation and subsumption functions. The third layer[11] contained the basic closure algorithm, which could be controlled interactively.
LMA exhibited the classic ``second system'' effect, in which a system contains every desirable feature and thus becomes cumbersome. It had Lisp and Prolog interfaces (including a built-in Prolog system callable in the middle of an inference), floating-point numbers, and an interactive help system. It was portable to Unix, VMS, and CMS operating systems, although it was most used on a VAX 11/780. The combination of its VAX home and its many data-hiding features made it slower than the earlier systems, but it could still do all of the old problems because of its extensive facilities for redundancy control. It was used for exploring areas outside mathematics and logic, such as puzzles, circuit design, etc. It could be used interactively to construct proofs that it could not find unaided.
LMA started another tradition. It was the first system to be widely distributed to others, along with documentation. Over 150 copies were given to outside users. John Kalman wrote a tutorial and workbook[4] to help the novice user.