A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
From MaRDI portal
Publication:5597535
DOI10.1145/321592.321603zbMath0199.31502OpenAlexW2010405422MaRDI QIDQ5597535
W. W. Bledsoe, Robert Brockett Anderson
Publication date: 1970
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321592.321603
Related Items
Completeness results for inequality provers, Hierarchical deduction, Formalization of the resolution calculus for first-order logic, Subsumption-linear Q-resolution for QBF theorem proving, Exploiting data dependencies in many-valued logics, Knowledge-based proof planning, A logic for programming with complex objects, The completeness of gp-resolution for annotated logics, Producing and verifying extremely large propositional refutations, Linearity and regularity with negation normal form, Experimental tests of resolution-based theorem-proving strategies, Model elimination without contrapositives, A mechanization of strong Kleene logic for partial functions, Resolution graphs, Splitting and reduction heuristics in automatic theorem proving, Linear resolution with selection function, Theorem proving with variable-constrained resolution, A note on linear resolution strategies in consequence-finding, On the refutational completeness of signed binary resolution and hyperresolution, A typed resolution principle for deduction with conditional typing theory, SET-VAR
