| The automated reasoning assistants otter and MACE are applied to the following open problem in equivalential calculus: which equivalential tautologies will serve as shortest single axioms with both condensed detachment and reversed condensed detachment as inference rules. Earlier uses of otter are extended and executed systematically using a generic driver program. The application of MACE to this problem required the development of new techniques. A description of the 630 possibilities is given, and seven new shortest single axioms are presented. All but five of the remaining possibilities (up to duality) are shown to be too weak, and it is noted that the above results supersede in some respects the results of a similar unpublished paper. |
Keywords
Math Review Classification
Last Updated
24/3/97
Length
38 pages
Availability
This article is available in: