propositional-logic resolution proof-theory
Definition
Derivation (Propositional Resolution)
In the propositional resolution calculus, a derivation from a set of clauses
is a sequence of clauses that starts with the input clauses and then adds clauses obtained by allowed inference steps. If
then a derivation from
has the form where
are the input clauses, and every derived clause with is either:
- a resolvent of earlier clauses
and , for some ; or - a factor of an earlier clause
, using the factoring inference rule, for some . A derivation is a refutation when one of its derived clauses is the empty clause
.