Semantic Paramodulation for Horn Sets

McCune, William; Henschen, Lawrence J.

Semantic Paramodulation for Horn Sets

Download BibTeX Cite

Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. 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 .

William McCune, and Lawrence J. Henschen. 1983. Semantic Paramodulation for Horn Sets. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83. IJCAI, 902–907. https://ijcai.org/proceedings/1983/213

@inproceedings{ijcai1983p213,
  title     = {Semantic Paramodulation for Horn Sets},
  author    = {McCune, William and Henschen, Lawrence J.},
  booktitle = {Proceedings of the Eighth International Joint Conference on
               Artificial Intelligence, {IJCAI-83}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Alan Bundy},
  pages     = {902--907},
  year      = {1983},
  note      = {Theorem Proving},
  url       = {https://ijcai.org/proceedings/1983/213},
}

TY  - CPAPER
TI  - Semantic Paramodulation for Horn Sets
AU  - McCune, William
AU  - Henschen, Lawrence J.
T2  - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1983
SP  - 902
EP  - 907
UR  - https://ijcai.org/proceedings/1983/213
ER  -