scientific article; zbMATH DE number 3278281
From MaRDI portal
Publication:5562604
zbMath0174.29202MaRDI QIDQ5562604
Publication date: 1967
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (16)
History and basic features of the critical-pair/completion procedure ⋮ Theorem proving with abstraction ⋮ Conditional equational theories and complete sets of transformations ⋮ A nucleus of a theorem-prover described inAlgol-68 ⋮ On the role of unification in mechanical theorem proving ⋮ An implementation of hyper-resolution ⋮ Complete sets of transformations for general E-unification ⋮ 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 ⋮ Horn equational theories and paramodulation ⋮ Linear resolution with selection function ⋮ Theorem proving with variable-constrained resolution ⋮ The linked conjunct method for automatic deduction and related search techniques ⋮ Set of support, demodulation, paramodulation: a historical perspective
This page was built for publication:
