scientific article; zbMATH DE number 7267153

DOI10.3969/J.ISSN.0258-2724.20180800MaRDI QIDQ5128049zbMATH OpenFDO

Authors Feng Cao, Yang Xu, Shuwei Chen, Guanfeng Wu, Wen-Jing Chang

Publication date 27 October 2020

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

zbMATH Keywords

artificial intelligencebinary resolutioncontradiction separation rulemathematical logictheorem proving

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

• Contradiction separation based dynamic multi-clause synergized automated deduction
• scientific article; zbMATH DE number 7267155
• Resolution-based theorem proving for many-valued logics
• scientific article; zbMATH DE number 1127072

Cited in

(4)

• Contradiction separation based dynamic multi-clause synergized automated deduction
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• A multi-clause dynamic deduction algorithm based on standard contradiction separation rule
• On structures of sign-boundary and diagonal vacancy-type standard contradictions

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 Q5128049)