OTTER Experiments Pertinent to CADE-10
Description:
This Argonne report serves as a companion to our CADE-10 paper. To fulfill promises made in that paper, included here are detailed proofs in clause notation, input files compatible with OTTER, and explanations for the choice of approach. Also included are certain of the original and unpublished proofs (of Winker) that answered four open questions, two in equivalent calculus and two in the R-calculus. The organization parallels that of the CADE-10 paper.
Date:
February 1991
Creator:
Wos, Larry; Winker, S.; McCune, W.; Overbeek, R.; Lusk, E.; Stevens, R. et al.
Partner:
UNT Libraries Government Documents Department