|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
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
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.
Math Review Classification
This article is available in: