---
title: "A Superposition Oriented Theorem Prover"
authors:
  - "Laurent Fribourg"
doi: ""
url: "https://ijcai.org/proceedings/1983/217"
pdf: "https://ijcai.org/proceedings/1983/0217.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "923-924"
track: "Theorem Proving"
keywords:
---

# A Superposition Oriented Theorem Prover

Laurent Fribourg

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 923-924.

## Abstract

A theorem proving procedure is described which combines the approach of locking resolution with that of rewriting systems. Indeed, both the binary resolution and a complete restriction of paramodulation are embodied by an extension of the rewriting operation called superposition. Experimental results are reported and compared with literature automated proofs.