An order-sorted resolution in theory and practice

AbstractSort systems are introduced to improve representation and manipulation of information. While no single system serves all needs, it turns out that a relatively simple order-sorted system is especially suited to, and expressive enough for a particular application in formal software verification. This system gives the desired powerful sort reasoner, boosting the resolution prover which underlies the verification tool.Our techniques use Frisch's hybrid model, which localises the sort information in the sort reasoner, and Walther's sorted unification algorithm. The originality of this work lies in realising such an upgrade. On the theoretical side, the necessary foundations are laid, ranging from syntax and semantics of the order-sorted first-order predicate logic to a completeness theorem for the calculus. On the practical level, a key issue is to obtain an efficiency gain in real terms. In theory, this is guaranteed under a subsort-meet closure assumption. In practice, we realise this by a non-iterative, single step extension process. The proposed order-sorted system passes the final feasibility check with its successful implementation and actual use in the verification application