A Many-Sorted Resolution Based on an Extension of a First-Order Language
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 1175-1176.
Abstract
A type of problern is first identified which may occur when a resolution scheme is applied to a many-sorted theory. To avoid euch a problem, an extension of the rlr!lt·order langnage called one-1orted language witla aggregale tJariable• is introduced. Aggregate variables allow the introduction of range-restricted variables dynamically in the structure which is expanded by definitions. This allows the introduction of a new resolution scheme called UWR-re10lution . It ean be shown that the UWR-resolution is more efficient than the existing schemes.
@inproceedings{ijcai1985p238,
title = {A Many-Sorted Resolution Based on an Extension of a First-Order Language},
author = {Irani, Keki B. and Shin, D. G.},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {1175--1176},
year = {1985},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1985/238},
}
TY - CPAPER TI - A Many-Sorted Resolution Based on an Extension of a First-Order Language AU - Irani, Keki B. AU - Shin, D. G. T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 1175 EP - 1176 UR - https://ijcai.org/proceedings/1985/238 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
