In this paper we present a solver for a first-order logic language where sets and binary relations can be freely and naturally combined. The language can express, at least, any full set relation algebra on finite sets. It provides untyped, hereditarily finite sets, whose elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Sets are first-class entities in the language, thus they are not encoded in lower level theories. Relations are just sets of ordered pairs. The solver exploits set unification and set constraint solving as primitive features. The solver is proved to be a sound semi-decision procedure for the accepted language. A Prolog implementation is presented and an extensive empirical evaluation provides evidence of its usefulness.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
More precisely, each solution of \(\varPhi \) expanded to the variables occurring in \(\varPhi _i\) but not in \(\varPhi \), so as to account for the possible fresh variables introduced into \(\varPhi _i\).
Actually there is some overlapping among these collections. This is difficult to avoid, as each author uses different variable names, the problem can be stated in slightly different ways (e.g., by applying commutativity) and even different names for the same operator are used (e.g., sum and union).
Most of the time is spent in solving 27 problems of tptp.bool encoding rather complex Boolean results where instead of using Boolean variables, we prove more general results by using finite set variables.