Resolution With Merging

DOI10.1145/321466.321469MaRDI QIDQ5573405zbMATH OpenOpenAlexFDO

Authors Peter B. Andrews

Publication date 1968

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/321466.321469

zbMATH Keywords

recursion theory, constructive mathematics

Cited in

(12)

• A fixpoint semantics of Horn sentences based on substitution sets
• Experimental tests of resolution-based theorem-proving strategies
• On the termination of clause graph resolution
• The linked conjunct method for automatic deduction and related search techniques
• Resolution graphs
• Extracting information from resolution proof trees
• Linear resolution with selection function
• Theorem proving with variable-constrained resolution
• What we can learn from conflicts in propositional satisfiability
• Labelled interpolation systems for hyper-resolution, clausal, and local proofs
• Ground Interpolation for Combined Theories
• RAT elimination

This page was built for publication: Resolution With Merging

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