scientific article; zbMATH DE number 7267155

DOI10.3969/J.ISSN.0258-2724.20180974MaRDI QIDQ5128050zbMATH OpenFDO

Authors Xinran Ning, Yang Xu, Xingxing He

Publication date 27 October 2020

Full work available at URL https://doi.org/10.3969/J.ISSN.0258-2724.20180974

zbMATH Keywords

clause elimination methodfirst-order logicimplication modulo resolutionpreprocessing techniqueset implication modulo resolution

Mathematics Subject Classification ID

Classical first-order logic (03B10) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• A unifying principle for clause elimination in first-order logic
• Extended First-Order Logic
• scientific article; zbMATH DE number 824731
• scientific article; zbMATH DE number 67452
• scientific article; zbMATH DE number 19145
• Unification in first-order transitive modal logic
• Fixed-point extensions of first-order logic
• scientific article; zbMATH DE number 1098495
• Publication:4503913
• Clause elimination procedures for CNF formulas

Cited in

(4)

• Set-blocked clause and extended set-blocked clause in first-order logic
• A unifying principle for clause elimination in first-order logic
• scientific article; zbMATH DE number 67452 (Why is no real title available?)
• scientific article; zbMATH DE number 7267153 (Why is no real title available?)

This page was built for publication:

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