Resolution With Merging

DOI10.1145/321466.321469zbMath0182.02506OpenAlexW2025360553MaRDI QIDQ5573405

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

Related Items

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