@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},
}

{"_id":"Pzeu2yjCpYXLnSA7u","bibbaseid":"weidenbach-dimova-fietzke-kumar-suda-wischnewski-spassversion35-2009","downloads":0,"creationDate":"2017-09-01T03:35:40.587Z","title":"SPASS Version 3.5","author_short":["Weidenbach, C.","Dimova, D.","Fietzke, A.","Kumar, R.","Suda, M.","Wischnewski, P."],"year":2009,"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/SilverSylvester","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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":[{"propositions":[],"lastnames":["Weidenbach"],"firstnames":["Christoph"],"suffixes":[]},{"propositions":[],"lastnames":["Dimova"],"firstnames":["Dilyana"],"suffixes":[]},{"propositions":[],"lastnames":["Fietzke"],"firstnames":["Arnaud"],"suffixes":[]},{"propositions":[],"lastnames":["Kumar"],"firstnames":["Rohit"],"suffixes":[]},{"propositions":[],"lastnames":["Suda"],"firstnames":["Martin"],"suffixes":[]},{"propositions":[],"lastnames":["Wischnewski"],"firstnames":["Patrick"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Schmidt"],"firstnames":["Renate","A."],"suffixes":[]}],"year":"2009","keywords":"Automate Theorem Prover, Empty Clause, Reduction Rule, Small Clause, Soft Typing","pages":"140–145","bibtex":"@inproceedings{weidenbach_spass_2009,\n\taddress = {Berlin, Heidelberg},\n\tseries = {Lecture {Notes} in {Computer} {Science}},\n\ttitle = {{SPASS} {Version} 3.5},\n\tisbn = {978-3-642-02959-2},\n\tdoi = {10/czdzbj},\n\tabstract = {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.},\n\tlanguage = {en},\n\tbooktitle = {Automated {Deduction} – {CADE}-22},\n\tpublisher = {Springer},\n\tauthor = {Weidenbach, Christoph and Dimova, Dilyana and Fietzke, Arnaud and Kumar, Rohit and Suda, Martin and Wischnewski, Patrick},\n\teditor = {Schmidt, Renate A.},\n\tyear = {2009},\n\tkeywords = {Automate Theorem Prover, Empty Clause, Reduction Rule, Small Clause, Soft Typing},\n\tpages = {140--145},\n}\n\n","author_short":["Weidenbach, C.","Dimova, D.","Fietzke, A.","Kumar, R.","Suda, M.","Wischnewski, P."],"editor_short":["Schmidt, R. A."],"key":"weidenbach_spass_2009","id":"weidenbach_spass_2009","bibbaseid":"weidenbach-dimova-fietzke-kumar-suda-wischnewski-spassversion35-2009","role":"author","urls":{},"keyword":["Automate Theorem Prover","Empty Clause","Reduction Rule","Small Clause","Soft Typing"],"metadata":{"authorlinks":{}},"html":""},"search_terms":["spass","version","weidenbach","dimova","fietzke","kumar","suda","wischnewski"],"keywords":["automate theorem prover","empty clause","reduction rule","small clause","soft typing"],"authorIDs":[],"dataSources":["8jafqMAWgB7XP4FTZ","YCBcQPneB9oxahSnp"]}