---
title: "A Many-Sorted Resolution Based on an Extension of a First-Order Language"
authors:
  - "Keki B. Irani"
  - "D. G. Shin"
doi: ""
url: "https://ijcai.org/proceedings/1985/238"
pdf: "https://ijcai.org/proceedings/1985/0238.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1175-1176"
track: "Theorem Proving"
keywords:
---

# A Many-Sorted Resolution Based on an Extension of a First-Order Language

Keki B. Irani, D. G. Shin

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, 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.