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是一款一阶定理证明器（first-order theorem prover），它实现了针对自下而上模型生成的高级阻塞（blocking）及其他增强技术。该实现基于对SPASS证明器的改造，以及Yarralumla中内置的公式变换（formula transformations）。 有关该理论、证明过程、实现方式，以及在TPTP基准测试集（TPTP benchmark suite）上的实证评估结果，可参阅以下文献： 《面向自下而上模型生成方法的阻塞及其他增强技术》（Blocking and Other Enhancements for Bottom-Up Model Generation Methods），作者P. Baumgartner与R. A. Schmidt，即将发表于《自动化推理期刊》（Journal of Automated Reasoning）。其短篇版本收录于Furbach, U. 及Shankar, N. 主编的《自动化推理：第三届国际自动化推理联合会议（IJCAR 2006）》（Automated Reasoning: Third International Joint Conference on Automated Reasoning (IJCAR 2006)），载于《人工智能讲义》（Lecture Notes in Artificial Intelligence）第4130卷，Springer出版社，第125-139页（2006年）。