A Many-Sorted Calculus Based on Resolution and Paramodulation
Proceedings of the Eighth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 882-890.
Abstract
The first-order ca l c ulus whose well formed formulas are clauses and whose sole inference rules are factorization, resolution and paramodulation is extended to a many-sorted calculus. As abasis for Automated Theorem Proving, this many-sorted calcu lus le ads to a remarka ble reduction of thesearch space and also to simpler proofs. The soundness and completeness of th e new ca lculus and the Sort-Theorem, which relate s t he many-sorted c alculus to its one -s o rt ed cou nterpart, are shown. Inaddition results about term rewriting a nd unification in a many-sorted calculus are obtained. Pra ctical examp l es and a proof protocol of an automated th eorem proverbased on the many-sorted calculus a re presented.
@inproceedings{ijcai1983p211,
title = {A Many-Sorted Calculus Based on Resolution and Paramodulation},
author = {Walther, Christoph},
booktitle = {Proceedings of the Eighth International Joint Conference on
Artificial Intelligence, {IJCAI-83}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Alan Bundy},
pages = {882--890},
year = {1983},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1983/211},
}
TY - CPAPER TI - A Many-Sorted Calculus Based on Resolution and Paramodulation AU - Walther, Christoph T2 - Proceedings of the Eighth International Joint Conference on Artificial Intelligence, IJCAI-83 PB - International Joint Conferences on Artificial Intelligence PY - 1983 SP - 882 EP - 890 UR - https://ijcai.org/proceedings/1983/211 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
