Shortest Single Axioms for the Equivalential Calculus with CD and RCD

Kahlil Hodgson


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

Last Updated

38 pages

This article is available in: