The Aquarius Theorem Prover
This is the code of the historic Aquarius theorem prover developed by Maria Paola Bonacina from January 1992 to December 1992. That was the last year of her PhD at the Department of Computer Science of the State University of New York at Stony Brook, New York, USA.
Aquarius was a parallel theorem prover based on the Clause-Diffusion methodology that Maria Paola Bonacina invented and described in her PhD thesis, which includes a chapter devoted to Aquarius:
Maria Paola Bonacina. Distributed automated deduction. Ph.D. Thesis, Department of Computer Science, State University of New York at Stony Brook, December 1992. Available at http://profs.sci.univr.it/~bonacina/pub_theses.html
Aquarius was a Clause-Diffusion prover for first-order logic with equality incorporating as sequential base the code of William W. (Bill) McCune's Otter (version 2.2).
Aquarius was written in C and PCN for workstation networks. This source code repository includes all .c files, .h files and a main .pcn file. It also includes a makefile showing how the binary, named m_penguin, was built.
After the PhD thesis, the Clause-Diffusion methodology and the Aquarius theorem prover were described in the following publications, written by Maria Paola Bonacina, co-authored with her PhD thesis advisor Jieh Hsiang, and listed here in reverse chronological order:
Maria Paola Bonacina and Jieh Hsiang. Distributed deduction by Clause-Diffusion: distributed contraction and the Aquarius prover. Journal of Symbolic Computation, 19:245-267, January-March 1995; DOI: 10.1006/jsco.1995.1014.
Maria Paola Bonacina and Jieh Hsiang. Distributed deduction by Clause-Diffusion: the Aquarius prover. In Proceedings of the Third International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO), Gmunden, Austria, September 1993. Springer, Lecture Notes in Computer Science 722, 272-287, 1993; DOI: 10.1007/BFb0013183.
Maria Paola Bonacina and Jieh Hsiang. A system for distributed simplification-based theorem proving. In Proceedings of the First International Workshop on Parallelization in Inference Systems, Schloss Dagstuhl, Germany, December 1990. Springer, Lecture Notes in Artificial Intelligence 590, 370-370, 1992; DOI: 10.1007/3-540-55425-4_18.
For further information on Clause-Diffusion see: http://profs.sci.univr.it/~bonacina/distributed.html
For further information on the Clause-Diffusion provers see: http://profs.sci.univr.it/~bonacina/cdprovers.html