SPASS Version 3.5. Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., & Wischnewski, P. In Automated Deduction – CADE-22, of Lecture Notes in Computer Science, pages 140–145, Berlin, Heidelberg, 2009. Springer.
doi  abstract   bibtex   
SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. This system description provides an overview of our recent developments in SPASS 3.5 including subterm contextual rewriting, improved split backtracking, a significantly faster FLOTTER implementation with additional control flags, completely symmetric implementation of forward and backward redundancy criteria, faster parsing with improved support for big files, faster and extended sort module, and support for include commands in input files. Finally, SPASS 3.5 can now parse files in TPTP syntax, comes with a new converter tptp2dfg and is distributed under a BSD style license.
@inproceedings{weidenbach_spass_2009,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {{SPASS} {Version} 3.5},
	isbn = {978-3-642-02959-2},
	doi = {10/czdzbj},
	abstract = {SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. This system description provides an overview of our recent developments in SPASS 3.5 including subterm contextual rewriting, improved split backtracking, a significantly faster FLOTTER implementation with additional control flags, completely symmetric implementation of forward and backward redundancy criteria, faster parsing with improved support for big files, faster and extended sort module, and support for include commands in input files. Finally, SPASS 3.5 can now parse files in TPTP syntax, comes with a new converter tptp2dfg and is distributed under a BSD style license.},
	language = {en},
	booktitle = {Automated {Deduction} – {CADE}-22},
	publisher = {Springer},
	author = {Weidenbach, Christoph and Dimova, Dilyana and Fietzke, Arnaud and Kumar, Rohit and Suda, Martin and Wischnewski, Patrick},
	editor = {Schmidt, Renate A.},
	year = {2009},
	keywords = {Automate Theorem Prover, Empty Clause, Reduction Rule, Small Clause, Soft Typing},
	pages = {140--145},
}

Downloads: 0