SPASS - Version 0.49
SPASS - Version 0.49
复制标题
SPASS - 版本 0.49
DOI：
10.1023/a:1005812220011
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Christoph Weidenbach
中科院分区：
文献类型：
--
作者：
Christoph Weidenbach
本文介绍SPASS，版本0.49，因为它是在CADE-13的系统竞争进入。SPASS是一个全一阶逻辑等式的自动定理证明器。它基于最初由Bachmair和Ganzinger开发的叠加演算，扩展了Weidenbach的排序技术和用于案例分析的推理规则。
This article describes SPASS, Version 0.49, as it was entered in the system competition at CADE-13. SPASS is an automated theorem prover for full first-order logic with equality. It is based on the superposition calculus originally developed by Bachmair and Ganzinger, extended by the sort techniques due to Weidenbach and an inference rule for case analysis.