Horn Unit Resolution (HORN)
Category: Logic
Input
A Horn formula $F$.
Problem
Can the empty clause $\Box$ be deduced from $F$ by unit resolution?
Definitions
A Horn formula is a conjunctive normal form (CNF) formula with each clause a disjunction of literals having at most one positive literal per clause.
Status
$\P$-complete (Dobkin, Lipton, and Reiss [1], Jones and Laaser [2]).
Remarks
References
- D. P. Dobkin, R. J. Lipton, and S. P. Reiss (1979). Linear programming is log-space hard for P.
- N. D. Jones and W. T. Laaser (1976). Complete problems for deterministic polynomial time.
- Greenlaw, R., Hoover, H. J., and Ruzzo, W. L. (1995). Limits to Parallel Computation: P-Completeness Theory. Oxford University Press. Problem A.6.2.