Unit propagation

Unit propagation (UP) or Boolean Constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of (usually propositional) clauses.

Horn satisfiability

Horn clause

Automated theorem proving

DPLL algorithm

Dowling, William F.; (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming, 1 (3): 267–284, doi:10.1016/0743-1066(84)90014-1, MR 0770156.

Gallier, Jean H.

H. Zhang and M. Stickel (1996). An efficient algorithm for unit-propagation. In Proceedings of the Fourth International Symposium on Artificial Intelligence and Mathematics.