Abstract: The Saturate system is an experimental theorem prover based on saturation. It has originally been developed as an implementation of the superposition calculus by Pilar Nivela and Robert Nieuwenhuis from the Technical University of Catalonia, Barcelona. The version the use of which is described in this document now contains extensions by chaining techniques for arbitrary transitive relations implemented by Harald Ganzinger, MPI Informatik, Saarbr{\"u}cken, with the help of Robert Nieuwenhuis.
Download: PostScript [gzip'd] (106 KBytes) | BibTeX-Entry[an error occurred while processing this directive]