Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
Case Splitting in an Automatic Theorem Prover for Real-Valued Special Functions
复制标题
实值特殊函数自动定理证明器中的案例分割
DOI：
10.1007/s10817-012-9245-6
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Bridge J
中科院分区：
文献类型：
--
作者：
Bridge J
案例拆分，有回溯和没有回溯，与直接有序解决进行比较。这两种形式的分裂已经在MetiTarski上实现，MetiTarski是一个实值特殊函数的自动定理证明器，例如，ln，sin，cos和tan− 1。实验结果证实了真实回溯优于通过引入新的谓词符号来模拟回溯，以及两者都优于直接归结。
Case splitting, with and without backtracking, is compared with straightforward ordered resolution. Both forms of splitting have been implemented for MetiTarski, an automatic theorem prover for real-valued special functions such as, ln , sin, cos and tan− 1. The experimental findings confirm the superiority of true backtracking over the simulation of backtracking through the introduction of new predicate symbols, and the superiority of both over straightforward resolution.
登录
查看更多内容
DOI：
--
发表时间：
2001
期刊：
International Joint Conference on Artificial Intelligence
影响因子：
--
作者：
A. Riazanov;A. Voronkov
通讯作者：
A. Voronkov
DOI：
10.1007/s10472-009-9150-9
发表时间：
2009-02-01
影响因子：
1.2
作者：
Fietzke, Arnaud;Weidenbach, Christoph
通讯作者：
Weidenbach, Christoph
通过新的命题符号进行分裂
DOI：
10.1007/3-540-45653-8_12
发表时间：
2001
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Hans de Nivelle
通讯作者：
Hans de Nivelle
SPASS - 版本 0.49
DOI：
10.1023/a:1005812220011
发表时间：
1997
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Christoph Weidenbach
通讯作者：
Christoph Weidenbach
自动定理证明工具的 TSTP 数据交换格式
DOI：
--
发表时间：
2004
期刊：
影响因子：
--
作者：
G. Sutcliffe;J. Zimmer;S. Schulz
通讯作者：
S. Schulz