scientific article; zbMATH DE number 3278281
From MaRDI portal
Publication:5562604
Cited in
(17)- History and basic features of the critical-pair/completion procedure
- Theorem proving with abstraction
- On the role of unification in mechanical theorem proving
- An implementation of hyper-resolution
- Complete sets of transformations for general E-unification
- Horn equational theories and paramodulation
- The linked conjunct method for automatic deduction and related search techniques
- Set of support, demodulation, paramodulation: a historical perspective
- An examination of the geometry theorem machine
- Renamable paramodulation for automatic theorem proving with equality
- Resolution graphs
- Finding resolution proofs and using duplicate goals in AND/OR trees
- Linear resolution with selection function
- Theorem proving with variable-constrained resolution
- A nucleus of a theorem-prover described inAlgol-68
- Confluence of conditional rewriting modulo
- Conditional equational theories and complete sets of transformations
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5562604)
