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 | ||
|---|---|---|---|
| Assertion | resolution | |- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ps \/ ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | simpr | |- ( ( ph /\ ps ) -> ps ) |
|
| 2 | simpr | |- ( ( -. ph /\ ch ) -> ch ) |
|
| 3 | 1 2 | orim12i | |- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ps \/ ch ) ) |