Resolution in propositional logic[edit]
$_$_$DEEZ_NUTS#0__subtitleDEEZ_NUTS$_$_$
Paramodulation[edit]
Paramodulation is a related technique for reasoning on sets of clauses where the predicate symbol is equality. It generates all "equal" versions of clauses, except reflexive identities. The paramodulation operation takes a positive from clause, which must contain an equality literal. It then searches an into clause with a subterm that unifies with one side of the equality. The subterm is then replaced by the other side of the equality. The general aim of paramodulation is to reduce the system to atoms, reducing the size of the terms when substituting.[17]
$_$_$DEEZ_NUTS#0__titleDEEZ_NUTS$_$_$
Resolution rule[edit]
The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two clauses containing complementary literals. A literal is a propositional variable or the negation of a propositional variable. Two literals are said to be complements if one is the negation of the other (in the following, is taken to be the complement to ). The resulting clause contains all the literals that do not have complements. Formally:
The clauses and are the inference's premises
(the resolvent of the premises) is its conclusion.
The literal is the left resolved literal,
The literal is the right resolved literal,
is the resolved atom or pivot.
is the most general unifier of the resolved literals.
![{\displaystyle [b/x]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/838f5c44f9a3f4ed28f7c1bd94f1873c154026c2)
Traugott's rule may yield a sharper resolvent: compare (5) and (10), which both resolve (1) and (2) on .
Due to the latter issue, Traugott's rule can take advantage of the implication in assumption (4), using as the in step (12). Using Murray's rules, the semantically equivalent formula was obtained as (7), however, it could not be used as due to its syntactic form.
