Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic --computational logic,mechanical theorem proving; G.1.6 [Numerical Analysis]: Optimization --integer programming; H.2.1 [Database Management]: Logical Design; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving --deduction,resolution

General Terms: Algorithms, Theory

Additional Key Words and Phrases: Horn clauses, propositional logic

Selected papers that cite this one

- Michel Conforti and Gérard Cornuéjols. A class of logic problems solvable by linear programming. Journal of the ACM, 42(5):1107-1113, September 1995.

- Vadim Kagan, Anil Nerode, and V. S. Subrahmanian. Computing minimal models by partial instantiation. Theoretical Computer Science, 155(1):157-177, 26 February 1996.

- Anil Nerode, Raymond T. Ng, and V. S. Subrahmanian. Computing circumscriptive databases: I. Theory and algorithms. Information and Computation, 116(1):58-80, January 1995.

- John S. Schlipf, Fred S. Annexstein, John V. Franco, and R. P. Swaminathan. On finding solutions for extended Horn formulas. Information Processing Letters, 54(3):133-137, 12 May 1995.

Selected references

- Stephen A. Cook. The complexity of theorem-proving procedures. In Conference Record of Third Annual ACM Symposium on Theory of Computing, pages 151-158, Shaker Heights, Ohio, 3-5 1971 1971.

- Susumu Yamasaki and Shuji Doshita. The satisfiability problem for a class consisting of Horn sentences and some non-Horn sentences in proportional logic. Information and Control, 59(1-3):1-12, October/November/December 1983.