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

zbMATH Keywords

natural deductiontheorem proving\(\lambda\)-calculuslogics of programming

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) 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
• Publication:4503919

Cited in

(10)

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

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)