Consolution and its Relation with Resolution

摘要

In this paper the method of consolution for clause form theorem proving is introduced. Consolution is based on the connection method. This means that in a consolution derivation the paths through the input formula are checked for complementarity. In contrast to resolution this checking can be done in a systematic way as in any connection calculus. It is proved that the consolution calculus presented here is sound and complete and that it can simulate resolution step by step and is a generalization of resolution. It combines the advantages of the connection method such as the directedness of search with the advantages of resolution such as the possibility of the use of lemmata.