---
title: "Semantic Paramodulation for Horn Sets"
authors:
  - "William McCune"
  - "Lawrence J. Henschen"
doi: ""
url: "https://ijcai.org/proceedings/1983/213"
pdf: "https://ijcai.org/proceedings/1983/0213.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "902-907"
track: "Theorem Proving"
keywords:
---

# Semantic Paramodulation for Horn Sets

William McCune, Lawrence J. Henschen

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 902-907.

## Abstract

We pr esen t a ne w s trategy for seman ti c paramodulation for Horn se t s and prove its compl e t e n e ss. Th e strategy require s for each par amo d ulation th at ei th er b ot h parents be fals e positive units or that on e parent and th e paramodulant both b e false relati ve t o an int erpretation. We also discuss so me of the issue s involve d in choosi ng an interpr etation th at has a ch ance of giving b etter pe r fo rmance th a t si mpl e set -of-supp ort par a modul atio n .