@INPROCEEDINGS{HustadtSchmidtWeidenbach98,
 AUTHOR    = {Hustadt, U. and Schmidt, R. A. and Weidenbach, C.},
 CMONTH    = may # {~5--8},
 YEAR      = {1998},
 TITLE     = {Optimised Functional Translation and Resolution},
 EDITOR    = {de Swart, H.},
 BOOKTITLE = {Proceddings of the International Conference on
 Automated Reasoning with Analytic Tableaux and Related Methods
 (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998]},
 SERIES    = {Lecture Notes in Computer Science},
 VOLUME    = {1397},
 PUBLISHER = {Springer},
 PAGES     = {36-37},
 URL       = {Hustadt+Schmidt+Weidenbach@TABLEAUX1998.pdf},
 URL       = {http://dx.doi.org/10.1007/3-540-69778-0_9},
 ABSTRACT  = {This paper describes our approach to modal theorem
 proving. We make use of a first-order theorem prover SPASS and a
 translation of modal logics to path logics via the optimised
 functional translation. Path logics are clausal logics over the
 language of the monadic fragment of sorted first-order logic with a
 special binary function symbol for defining accessibility. Clauses of
 path logics are restricted in that only Skolem terms which are
 constants may occur and the prefix stability property holds. Ordinary
 resolution without any refinement strategies is a decision procedure
 for the path logics associated with K(m) and KT(m). Our decision
 procedure for S4 uses an a priori term depth bound. SPASS uses ordered
 resolution and ordered factoring, it supports splitting and branch
 condensing (splitting amounts to case analysis while branch condensing
 resembles branch pruning in the Logics Workbench), it has an extensive
 set of reduction rules including tautology deletion, subsumption and
 condensing, and it supports dynamic sort theories by additional
 inference and reduction rules.}
}

{"_id":"pri9RwqpP7BBChBCC","bibbaseid":"hustadt-schmidt-weidenbach-optimisedfunctionaltranslationandresolution-1998","author_short":["Hustadt, U.","Schmidt, R. A.","Weidenbach, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]},{"propositions":[],"lastnames":["Schmidt"],"firstnames":["R.","A."],"suffixes":[]},{"propositions":[],"lastnames":["Weidenbach"],"firstnames":["C."],"suffixes":[]}],"cmonth":"May 5–8","year":"1998","title":"Optimised Functional Translation and Resolution","editor":[{"propositions":["de"],"lastnames":["Swart"],"firstnames":["H."],"suffixes":[]}],"booktitle":"Proceddings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998]","series":"Lecture Notes in Computer Science","volume":"1397","publisher":"Springer","pages":"36-37","url":"http://dx.doi.org/10.1007/3-540-69778-0_9","abstract":"This paper describes our approach to modal theorem proving. We make use of a first-order theorem prover SPASS and a translation of modal logics to path logics via the optimised functional translation. Path logics are clausal logics over the language of the monadic fragment of sorted first-order logic with a special binary function symbol for defining accessibility. Clauses of path logics are restricted in that only Skolem terms which are constants may occur and the prefix stability property holds. Ordinary resolution without any refinement strategies is a decision procedure for the path logics associated with K(m) and KT(m). Our decision procedure for S4 uses an a priori term depth bound. SPASS uses ordered resolution and ordered factoring, it supports splitting and branch condensing (splitting amounts to case analysis while branch condensing resembles branch pruning in the Logics Workbench), it has an extensive set of reduction rules including tautology deletion, subsumption and condensing, and it supports dynamic sort theories by additional inference and reduction rules.","bibtex":"@INPROCEEDINGS{HustadtSchmidtWeidenbach98,\n AUTHOR = {Hustadt, U. and Schmidt, R. A. and Weidenbach, C.},\n CMONTH = may # {~5--8},\n YEAR = {1998},\n TITLE = {Optimised Functional Translation and Resolution},\n EDITOR = {de Swart, H.},\n BOOKTITLE = {Proceddings of the International Conference on\n Automated Reasoning with Analytic Tableaux and Related Methods\n (TABLEAUX'98) [Oisterwijk, The Netherlands, 5-8 May 1998]},\n SERIES = {Lecture Notes in Computer Science},\n VOLUME = {1397},\n PUBLISHER = {Springer},\n PAGES = {36-37},\n URL = {Hustadt+Schmidt+Weidenbach@TABLEAUX1998.pdf},\n URL = {http://dx.doi.org/10.1007/3-540-69778-0_9},\n ABSTRACT = {This paper describes our approach to modal theorem\n proving. We make use of a first-order theorem prover SPASS and a\n translation of modal logics to path logics via the optimised\n functional translation. Path logics are clausal logics over the\n language of the monadic fragment of sorted first-order logic with a\n special binary function symbol for defining accessibility. Clauses of\n path logics are restricted in that only Skolem terms which are\n constants may occur and the prefix stability property holds. Ordinary\n resolution without any refinement strategies is a decision procedure\n for the path logics associated with K(m) and KT(m). Our decision\n procedure for S4 uses an a priori term depth bound. SPASS uses ordered\n resolution and ordered factoring, it supports splitting and branch\n condensing (splitting amounts to case analysis while branch condensing\n resembles branch pruning in the Logics Workbench), it has an extensive\n set of reduction rules including tautology deletion, subsumption and\n condensing, and it supports dynamic sort theories by additional\n inference and reduction rules.}\n}\n\n","author_short":["Hustadt, U.","Schmidt, R. A.","Weidenbach, C."],"editor_short":["de Swart, H."],"key":"HustadtSchmidtWeidenbach98","id":"HustadtSchmidtWeidenbach98","bibbaseid":"hustadt-schmidt-weidenbach-optimisedfunctionaltranslationandresolution-1998","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/3-540-69778-0_9"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["optimised","functional","translation","resolution","hustadt","schmidt","weidenbach"],"title":"Optimised Functional Translation and Resolution","year":1998}