---
title: "Equality Reasoning in Clause Graphics"
authors:
  - "Karl-Hans Bläsius"
doi: ""
url: "https://ijcai.org/proceedings/1983/221"
pdf: "https://ijcai.org/proceedings/1983/0221.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "936-938"
track: "Theorem Proving"
keywords:
---

# Equality Reasoning in Clause Graphics

Karl-Hans Bläsius

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 936-938.

## Abstract

A method to control the application of equalityderivation rules in an automatic theorem proving system is presented . When handling eq uality in the search for a pro o f of a theorem two main problems arise: 1) to obtain a control mechanism for the s ea r ch and application of useful equality derivation steps in order to support global strategies which plan and control the whole proof , thus conducing to an efficient and complete proof procedure. 2) to find proper equations rendering two t e rms unifiable. Thes e pr ob lems are solved by combining th e c laus e graph method and the "paramodulation-if-needed" idea by introducing Morris' E-resolution into th e clause graph proof procedure. The n eces sary equations to form possible E-resolvents are searched for in th e initial graph and are inh e rited afterwards. Th e search space f o r possible E -resolutions will be r ed uced by exploiting constraints using th e information in the clause graph.