Deciding in HFS-theory via linear integer programming. (English) Zbl 0790.90052

Voronkov, Andrei (ed.), Logic programming and automated reasoning. 4th international conference, LPAR ’93, St. Petersburg, Russia, July 13-20, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 698, 170-181 (1993).
Summary: We give a reduction, in polynomially bounded time, of the satisfiability problem in the set language MPLS, to an equivalent linear integer programming problem. We show that this provides an algorithm to decide the set unification problem. The procedure obtains the eventual unifiers of two set terms (i.e. at least a minimal exhaustive collection of unifiers) in “compact form”. The unifiers are given via the solutions of a linear integer system generated by the reduction. We also report further results concerning the construction of models over the atoms of the universe HFSA (the set model conceived here). These predict the number of useful atoms needed to produce a model of formulae involving the negation.
For the entire collection see [Zbl 0875.00121].


90C10 Integer programming
68T27 Logic in artificial intelligence