Theorem-Proving for Computers: Some Results on Resolution and Renaming

DOI10.1093/COMJNL/8.4.341MaRDI QIDQ5541352zbMATH OpenOpenAlexFDO

Authors B. Meltzer

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

zbMATH Keywords

mathematical logic

Cited in

(13)

• Renamable paramodulation for automatic theorem proving with equality
• Finding resolution proofs and using duplicate goals in AND/OR trees
• Completeness of resolution revisited
• Homomorphisms of conjunctive normal forms.
• Négation constructive et axiomatique interne
• MRPPS?An interactive refutation proof procedure system for question-answering
• Experimental tests of resolution-based theorem-proving strategies
• Parsing as non-Horn deduction
• Theorem proving with variable-constrained resolution
• A linear algorithm for renaming a set of clauses as a Horn set
• Struktursätze der Algebra und Kompliziertheit logischer Schemata. III Algebraische Theorien und Verallgemeinerungen
• Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.
• Beweisalgorithmen für die Prädikatenlogik

This page was built for publication: Theorem-Proving for Computers: Some Results on Resolution and Renaming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5541352)