Overview on mechanized theorem proving

DOI10.13328/J.CNKI.JOS.005870MaRDI QIDQ3308161zbMATH OpenFDO

Authors Nan Jiang, Qingan Li, Lumeng Wang, Xiaotong Zhang, Yanxiang He

Publication date 12 August 2020

Full work available at URL https://doi.org/10.13328/J.CNKI.JOS.005870

zbMATH Keywords

\(\lambda\)-calculuslogics of programmingnatural deductiontheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 2177632
• Computer theorem proving in mathematics
• scientific article; zbMATH DE number 1746646
• scientific article; zbMATH DE number 1100750
• scientific article; zbMATH DE number 1507199

Cited in

(10)

• Theorem proving in technology transfer: The user's point of view
• Mechanized result verification: An industrial application
• Automated theorem proving for special functions: the next phase
• Mechanical software verification: high level control aspects from a user's perspective
• Pervasive parallelism in highly-trustable interactive theorem proving systems
• scientific article; zbMATH DE number 2177632 (Why is no real title available?)
• scientific article; zbMATH DE number 2127501 (Why is no real title available?)
• scientific article; zbMATH DE number 4155933 (Why is no real title available?)
• scientific article; zbMATH DE number 1746646 (Why is no real title available?)
• Fully reusing clause deduction algorithm based on standard contradiction separation rule

This page was built for publication: Overview on mechanized theorem proving

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