Theorem-Proving for Computers: Some Results on Resolution and Renaming
From MaRDI portal
Publication:5541352
DOI10.1093/comjnl/8.4.341zbMath0158.26004OpenAlexW2109964311MaRDI QIDQ5541352
Publication date: 1966
Published in: The Computer Journal (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1093/comjnl/8.4.341
Related Items (13)
Homomorphisms of conjunctive normal forms. ⋮ Completeness of resolution revisited ⋮ Struktursätze der Algebra und Kompliziertheit logischer Schemata. III Algebraische Theorien und Verallgemeinerungen ⋮ Parsing as non-Horn deduction ⋮ Négation constructive et axiomatique interne ⋮ Experimental tests of resolution-based theorem-proving strategies ⋮ Renamable paramodulation for automatic theorem proving with equality ⋮ Finding resolution proofs and using duplicate goals in AND/OR trees ⋮ Theorem proving with variable-constrained resolution ⋮ Beweisalgorithmen für die Prädikatenlogik ⋮ Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. ⋮ MRPPS?An interactive refutation proof procedure system for question-answering ⋮ A linear algorithm for renaming a set of clauses as a Horn set
This page was built for publication: Theorem-Proving for Computers: Some Results on Resolution and Renaming
