---
title: "Consolution and its Relation with Resolution"
authors:
  - "Elmar Eder"
doi: ""
url: "https://ijcai.org/proceedings/1991/20"
pdf: "https://ijcai.org/proceedings/1991/0020.pdf"
venue: "Proceedings of the Twelfth International Joint Conference on Artificial Intelligence"
year: 1991
pages: "132-135"
track: "Automated Reasoning"
keywords:
---

# Consolution and its Relation with Resolution

Elmar Eder

*Proceedings of the Twelfth International Joint Conference on Artificial Intelligence*, pages 132-135.

## Abstract

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.