A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 1162-1167.
Abstract
A m~t~Y-tor1ed firll ord« calculUI, c:aUtd I:RP [Wa83] . whoee weU rormed rorau&u are typed clauses and wbose lnference rulea are faclcltiatioft. resolution, paramodulation and wea.teain& is extended to a many lOtted calculus EJtP• witb polymorphic funcüons (overloacfula) . lt il assumed tbat tbe l<l't structure is a f.iftite partialty ordered Mt witb a areatest element. It is sbown, tbat this extended calculus is sound and compJete, provided tbe runctioall reflelivity alioas are prnent. It il also sbown, tbat unification ct term1 containing polymorpbic functions is in &eftefal finitary, i.e. tbe set d most aeneral unifiers may contain more tban one element, but at most finitely many. We give a natural condition for tbe sianature (the sort structure ). sucb tbat the set of most leftefal uniliera is a.tways at most a singleton provided tbis conditioft bolds.
@inproceedings{ijcai1985p236,
title = {A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation},
author = {Schmidt-Schauß, Manfred},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {1162--1167},
year = {1985},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1985/236},
}
TY - CPAPER TI - A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation AU - Schmidt-Schauß, Manfred T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 1162 EP - 1167 UR - https://ijcai.org/proceedings/1985/236 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
