![]() |
Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > resolution | Structured version Visualization version GIF version |
Description: Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.) |
Ref | Expression |
---|---|
resolution | ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 488 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
2 | simpr 488 | . 2 ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | orim12i 906 | 1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∨ wo 844 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |