Mathbox for David A. Wheeler |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > resolution | Structured version Visualization version Unicode 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 477 | . 2 | |
2 | simpr 477 | . 2 | |
3 | 1, 2 | orim12i 538 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wo 383 wa 384 |
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 197 df-or 385 df-an 386 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |