A Resolution Calculus with Dynamic Sort Structures and Partial Functions

Abstract

A many sorted logic is presented, which supports partial functions as well as potentially empty sorts and the dynamic derivation of sort information. In this so called DSPF-logic1 (Dynamic Sorts and Partial Functions), the specification of the sort structure and the declarations for constant and function symbols are part of the formulae themselves. Therefore sort information needs not necessarily be known from the beginning but can be deduced from other information. Nevertheless the resolution calculus which is presented is almost as restrictive as in logics with static sort information.