@INPROCEEDINGS{Schmidt+Hustadt@CADE2000,
 AUTHOR    = {Schmidt, R. A. and Hustadt, U.},
 CMONTH     = jun # {~17--20,},
 CYEAR      = {2000},
 YEAR      = {2000},
 TITLE     = {A Resolution Decision Procedure for Fluted Logic},
 EDITOR    = {McAllester, D.},
 BOOKTITLE = {Proceedings of the 17th International Conference
 on Automated Deduction (CADE-17)</em> [Pittsburgh, USA, 17-20 June2000]},
 SERIES    = {Lecture Notes in Artificial Intelligence},
 VOLUME    = {1831},
 PUBLISHER = {Springer},
 PAGES     = {433-448},
 URL       = {Schmidt+Hustadt@CADE2000.pdf},
 URL       = {http://dx.doi.org/10.1007/10721959_34},
 ABSTRACT = {Fluted logic is a fragment of first-order logic without
 function symbols in which the arguments of atomic subformulae form
 ordered sequences. A consequence of this restriction is that, whereas
 first-order logic is only semi-decidable, fluted logic is decidable.
 In this paper we present a sound, complete and terminating inference
 procedure for fluted logic. Our characterisation of fluted logic is in
 terms of a new class of so-called fluted clauses. We show that this
 class is decidable by an ordering refinement of first-order resolution
 and a new form of dynamic renaming, called separation.} 
}

{"_id":"pCGwr8sdscQZquHf4","bibbaseid":"schmidt-hustadt-aresolutiondecisionprocedureforflutedlogic-2000","author_short":["Schmidt, R. A.","Hustadt, U."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Schmidt"],"firstnames":["R.","A."],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]}],"cmonth":"June 17–20,","cyear":"2000","year":"2000","title":"A Resolution Decision Procedure for Fluted Logic","editor":[{"propositions":[],"lastnames":["McAllester"],"firstnames":["D."],"suffixes":[]}],"booktitle":"Proceedings of the 17th International Conference on Automated Deduction (CADE-17)</em> [Pittsburgh, USA, 17-20 June2000]","series":"Lecture Notes in Artificial Intelligence","volume":"1831","publisher":"Springer","pages":"433-448","url":"http://dx.doi.org/10.1007/10721959_34","abstract":"Fluted logic is a fragment of first-order logic without function symbols in which the arguments of atomic subformulae form ordered sequences. A consequence of this restriction is that, whereas first-order logic is only semi-decidable, fluted logic is decidable. In this paper we present a sound, complete and terminating inference procedure for fluted logic. Our characterisation of fluted logic is in terms of a new class of so-called fluted clauses. We show that this class is decidable by an ordering refinement of first-order resolution and a new form of dynamic renaming, called separation.","bibtex":"@INPROCEEDINGS{Schmidt+Hustadt@CADE2000,\n AUTHOR = {Schmidt, R. A. and Hustadt, U.},\n CMONTH = jun # {~17--20,},\n CYEAR = {2000},\n YEAR = {2000},\n TITLE = {A Resolution Decision Procedure for Fluted Logic},\n EDITOR = {McAllester, D.},\n BOOKTITLE = {Proceedings of the 17th International Conference\n on Automated Deduction (CADE-17)</em> [Pittsburgh, USA, 17-20 June2000]},\n SERIES = {Lecture Notes in Artificial Intelligence},\n VOLUME = {1831},\n PUBLISHER = {Springer},\n PAGES = {433-448},\n URL = {Schmidt+Hustadt@CADE2000.pdf},\n URL = {http://dx.doi.org/10.1007/10721959_34},\n ABSTRACT = {Fluted logic is a fragment of first-order logic without\n function symbols in which the arguments of atomic subformulae form\n ordered sequences. A consequence of this restriction is that, whereas\n first-order logic is only semi-decidable, fluted logic is decidable.\n In this paper we present a sound, complete and terminating inference\n procedure for fluted logic. Our characterisation of fluted logic is in\n terms of a new class of so-called fluted clauses. We show that this\n class is decidable by an ordering refinement of first-order resolution\n and a new form of dynamic renaming, called separation.} \n}\n\n\n","author_short":["Schmidt, R. A.","Hustadt, U."],"editor_short":["McAllester, D."],"key":"Schmidt+Hustadt@CADE2000","id":"Schmidt+Hustadt@CADE2000","bibbaseid":"schmidt-hustadt-aresolutiondecisionprocedureforflutedlogic-2000","role":"author","urls":{"Paper":"http://dx.doi.org/10.1007/10721959_34"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["resolution","decision","procedure","fluted","logic","schmidt","hustadt"],"title":"A Resolution Decision Procedure for Fluted Logic","year":2000}