Logical inference and polyhedral projection. (English) Zbl 0819.68105

Börger, Egon (ed.) et al., Computer science logic. 5th workshop, CSL ’91, Berne, Switzerland, October 7-11, 1991. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 626, 184-200 (1992).
If a (medical diagnosis) knowledge base contains atomic propositions \(x_ 1,\dots, x_ n\), and \(x_ 1,\dots, x_ k\) are the disease propositions, then finding all implies propositions that contain no other atoms but \(x_ 1,\dots, x_ k\) is a problem of projecting the knowledge base onto the variables \(x_ 1,\dots, x_ k\), and that is problem closely related to projecting a polyhedron. The main result of the paper is that polyhedral projection obtains precisely the inferences derived by a certain form of unit resolution, called unit \(K\)-resolution, which becomes unit resolution if all atoms in \(x_ 1,\dots, x_ k\) are erased. Unit \(K\)-resolution is proved to completely solve the logical projection problem for Horn clauses, that resolution algorithm is exponential when \(\underline n\) is proportional to \(\underline k\), but (quadratic) polynomial when \(\underline k\) is fixed. A number of new satisfiability algorithms are defined on the basis of polyhedral projection interpretation as inference method in propositional logic.
For the entire collection see [Zbl 0772.68004].
Reviewer: N.Curteanu (Iaşi)


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T35 Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
03B20 Subsystems of classical logic (including intuitionistic logic)