Case splitting in an automatic theorem prover for real-valued special functions
From MaRDI portal
(Redirected from Publication:352970)
Recommendations
- Automated theorem proving for special functions: the next phase
- MetiTarski: An automatic theorem prover for real-valued special functions
- A case study in automated theorem proving: Finding sages in combinatory logic
- Proof automation for functional correctness in separation logic
- scientific article; zbMATH DE number 2014706
- Foundations of a theorem prover for functional and mathematical uses
- scientific article; zbMATH DE number 800143
- scientific article; zbMATH DE number 4074542
- Automated theorem proving for assertions in separation logic with all connectives
- Using theory interpretation to mechanise the reals in a theorem prover
Cites work
- scientific article; zbMATH DE number 3338292 (Why is no real title available?)
- Combining superposition, sorts and splitting
- Computing small clause normal forms
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Labelled splitting
- Lightweight relevance filtering for machine-generated resolution problems
- MetiTarski: An automatic theorem prover for real-valued special functions
- Resolution theorem proving
- Splitting through new proposition symbols
This page was built for publication: Case splitting in an automatic theorem prover for real-valued special functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q352970)
