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)

MSC:

 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)