Implicational completeness of signed resolution

DOI10.1007/3-540-46508-1_11MaRDI QIDQ4503909zbMATH OpenFDO

Authors Christian G. Fermüller

Publication date 4 June 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-46508-1_11

zbMATH Keywords

implicational completenessresolutionsigned logics

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Review text

Implicational completeness for resolution means that, given a set \(\mathcal {S}\) of clauses, for every non-tautological clause \(C\) that is logically implied by \(\mathcal {S}\) there exists a clause \(D\) which subsumes \(C\) and it is derivable by resolution from \(\mathcal {S}\). This result was first proved by R. C. T. Lee in his PhD thesis in 1967, but it is not often mentioned in either books or papers on the subject, mainly due to the fact that it does not hold in the majority of the refinements of Robinson's original method. The paper presents a new proof of implicational completeness of resolution in the more general setting of signed logics (which subsumes any first-order finite-valued logic). The structure of the proof is much clearer than the original one and, in addition, it follows in a surprisingly straightforward manner from the standard idea of semantic trees. For the entire collection see [Zbl 0933.00012].

Recommendations

• On the refutational completeness of signed binary resolution and hyperresolution
• scientific article; zbMATH DE number 4022664
• The Completeness of Propositional Resolution: A Simple and Constructive Proof
• Completeness of resolution revisited
• scientific article; zbMATH DE number 8781

This page was built for publication: Implicational completeness of signed resolution

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