feret@qucis.UUCP (Michel Feret) (06/28/88)
I'm currently working on an implementation of a Resolution theorem prover written in Nial (Nested Interactive Array Language) . Nial uses nested multi-dimensional collections of basic objects (integers, truth values, complex numbers, ...) called nested arrays. We are using these arrays as logical terms in the logic programming component of Nial . I'm looking for theorem provers using more complex data structures than lists, and being able to perform unification over these data structures. Any references, pointers, addresses, ... will be welcomed. Michel Feret.