A Superposition Oriented Theorem Prover
Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. 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.
Laurent Fribourg. 1983. A Superposition Oriented Theorem Prover. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83. IJCAI, 923–924. https://ijcai.org/proceedings/1983/217
Fribourg, L. (1983). A Superposition Oriented Theorem Prover. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83 (pp. 923–924). IJCAI. https://ijcai.org/proceedings/1983/217
@inproceedings{ijcai1983p217,
title = {A Superposition Oriented Theorem Prover},
author = {Fribourg, Laurent},
booktitle = {Proceedings of the Eighth International Joint Conference on
Artificial Intelligence, {IJCAI-83}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Alan Bundy},
pages = {923--924},
year = {1983},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1983/217},
}
TY - CPAPER TI - A Superposition Oriented Theorem Prover AU - Fribourg, Laurent T2 - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83 PB - International Joint Conferences on Artificial Intelligence PY - 1983 SP - 923 EP - 924 UR - https://ijcai.org/proceedings/1983/217 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
