Automated theorem proving for special functions: the next phase

DOI10.1145/2631948.2631950MaRDI QIDQ2819703zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Lawrence C. Paulson

Publication date 29 September 2016

Published in Proceedings of the 2014 Symposium on Symbolic-Numeric Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2631948.2631950

zbMATH Keywords

decision procedurestheorem proving

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 3938594
• scientific article; zbMATH DE number 1100750
• Progress in the Development of Automated Theorem Proving for Higher-Order Logic
• MetiTarski: An automatic theorem prover for real-valued special functions
• Overview on mechanized theorem proving

Cited in

(3)

• Case splitting in an automatic theorem prover for real-valued special functions
• A mechanical proof of the Church-Rosser theorem
• MetiTarski: An automatic theorem prover for real-valued special functions

Describes a project that uses

Uses Software

• Isabelle
• QEPCAD
• MetiTarski
• PVS
• Coq
• Isabelle/HOL
• OTTER

This page was built for publication: Automated theorem proving for special functions: the next phase

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