Subsumption and connection graphs

Abstract

A subsumption test based on the principal idea of Kowalski'sconnection graph proof procedure is developed. In contrast to the standard test this new test is sufficiently efficient to permit the unrestricted use of the subsumption rule in practice. The test is not limited to the connection graph proof procedure, but most naturally embedded into it. In the latter case the unrestricted combination of subsumption with other deletion rules is shown to be inconsistent.