Case splitting in an automatic theorem prover for real-valued special functions

DOI10.1007/s10817-012-9245-6zbMath1361.68187OpenAlexW2061644010WikidataQ57382569 ScholiaQ57382569MaRDI QIDQ352970

Lawrence Charles Paulson, James P. Bridge

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

zbMATH Keywords

splittingMetiTarskiresolution theorem provingSPASS

Mathematics Subject Classification ID

Uses Software

• MetiTarski
• OTTER
• SPASS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• MetiTarski: An automatic theorem prover for real-valued special functions
• Lightweight relevance filtering for machine-generated resolution problems
• Labelled splitting
• Splitting through New Proposition Symbols
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

This page was built for publication: Case splitting in an automatic theorem prover for real-valued special functions