Case splitting in an automatic theorem prover for real-valued special functions
From MaRDI portal
Publication:352970
DOI10.1007/S10817-012-9245-6zbMATH Open1361.68187OpenAlexW2061644010WikidataQ57382569 ScholiaQ57382569MaRDI QIDQ352970FDOQ352970
Authors: James P. Bridge, Lawrence C. Paulson 
Publication date: 5 July 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-012-9245-6
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
- Resolution theorem proving
- Title not available (Why is that?)
- Lightweight relevance filtering for machine-generated resolution problems
- Combining superposition, sorts and splitting
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- MetiTarski: An automatic theorem prover for real-valued special functions
- Labelled splitting
- Computing small clause normal forms
- Splitting through new proposition symbols
Cited In (1)
Uses Software
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)
