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 476 | . 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓) | |
2 | simpr 476 | . 2 ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜒) | |
3 | 1, 2 | orim12i 537 | 1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → (𝜓 ∨ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 382 ∧ wa 383 |
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 196 df-or 384 df-an 385 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |