SPASS-Yarralumla

SPASS-yarralumla is a first-order theorem prover. It implements sophisticated forms of blocking and other enhanced techniques for bottom-up model generation. The implementation is based on an adaptation of the SPASS prover and formula transformations implemented in Yarralumla.

Details of the theory, proofs, the implementation and results of an empirical evaluation on problems from the TPTP benchmark suite can be found here:

Blocking and Other Enhancements for Bottom-Up Model Generation Methods. P. Baumgartner and R. A. Schmidt. To appear in the Journal of Automated Reasoning. The short version appears in Furbach, U. and Shankar, N. (eds), Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, Vol. 4130, Springer, 125-139 (2006).

SPASS-yarralumla乃一种一阶定理证明器，其实现了针对自底向上的模型生成的高级阻塞及其他增强技术。该实现基于对SPASS证明器和Yarralumla中公式转换的改编。关于该理论、证明、实现及对TPTP基准测试集中问题的实证评估结果的详细信息，可参见以下文献：《自底向上模型生成方法的阻塞及其他增强》。P. Baumgartner和R. A. Schmidt著。即将发表于《自动推理》期刊。简版已收录于Furbach, U.和Shankar, N.（编），《自动化推理：第三国际自动化推理联合会议（IJCAR 2006）》论文集。Springer人工智能系列，第4130卷，125-139页（2006年）。