Case splitting in an automatic theorem prover for real-valued special functions
type: Item
instance of: scholarly article
title: Case splitting in an automatic theorem prover for real-valued special functions
zbMATH Open document ID: 1361.68187
author: James P. Bridge
author: Lawrence C. Paulson
published in: Journal of Automated Reasoning
publication date: 2013-07-05T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6184688
zbMATH Keywords: splitting
zbMATH Keywords: resolution theorem proving
zbMATH Keywords: SPASS
zbMATH Keywords: MetiTarski
describes a project that uses: OTTER
describes a project that uses: SPASS
describes a project that uses: MetiTarski
MaRDI profile type: Publication
full work available at URL: s10817-012-9245-6
OpenAlex ID: W2061644010
Wikidata QID: Q57382569
cites work: MetiTarski: An automatic theorem prover for real-valued special functions
cites work: Resolution theorem proving
cites work: Labelled splitting
cites work: Lightweight relevance filtering for machine-generated resolution problems
cites work: Q5615207
cites work: Splitting through New Proposition Symbols
cites work: Computing small clause normal forms
cites work: Combining superposition, sorts and splitting
cites work: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
DOI: 10.1007/S10817-012-9245-6
Recommended article: Automated theorem proving for special functions: the next phase
Recommended article: MetiTarski: An automatic theorem prover for real-valued special functions
Recommended article: A case study in automated theorem proving: Finding sages in combinatory logic
Recommended article: Proof automation for functional correctness in separation logic
Recommended article: Q4437963
Recommended article: Foundations of a theorem prover for functional and mathematical uses
Recommended article: Q4848888
Recommended article: Q3805962
Recommended article: Automated Theorem Proving for Assertions in Separation Logic with All Connectives
Recommended article: Using theory interpretation to mechanise the reals in a theorem prover
description: scientific article; zbMATH DE number 6184688