Rewrite-based equational theorem proving with selection and simplification. (English) Zbl 0814.68117
An abstract notion of redundancy that does not affect refutational completeness is put to reduce search space in theorem proving for several first-order calculi with equality that admit any selection of negative literals.
Reviewer: M.Armbrust (Köln)
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
| 03B10 | Classical first-order logic |
| 68Q42 | Grammars and rewriting systems |
