A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness

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

zbMATH Keywords

languages, automata, networks

Related Items (21)

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

This page was built for publication: A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness