SPASS - Version 0.49

被引：25

作者：

Weidenbach, C ^{[1
]}

机构：

[1] MAX PLANCK INST INFORMAT,SAARBRUCKEN,GERMANY

来源：

JOURNAL OF AUTOMATED REASONING | 1997年 / 18卷 / 02期

关键词：

automated theorem proving; competition; SPASS; sorts; superposition;

D O I：

10.1023/A:1005812220011

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.

引用

页码：247 / 252

页数：6

共 7 条

[1]

Bachmair L., 1994, Journal of Logic and Computation, V4, P217, DOI 10.1093/logcom/4.3.217

[2] BASIC PARAMODULATION [J].