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

DOI10.1093/COMJNL/8.4.341zbMATH Open0158.26004OpenAlexW2109964311MaRDI QIDQ5541352FDOQ5541352

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)

• Parsing as non-Horn deduction
• Homomorphisms of conjunctive normal forms.
• Experimental tests of resolution-based theorem-proving strategies
• 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.
• MRPPS?An interactive refutation proof procedure system for question-answering
• A linear algorithm for renaming a set of clauses as a Horn set
• Theorem proving with variable-constrained resolution
• Renamable paramodulation for automatic theorem proving with equality
• Finding resolution proofs and using duplicate goals in AND/OR trees
• Beweisalgorithmen für die Prädikatenlogik
• Négation constructive et axiomatique interne
• Completeness of resolution revisited

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)