@ARTICLE{Ludwig+Hustadt@AIC2010,
 AUTHOR   = {Ludwig, Michel and Hustadt, Ullrich},
 TITLE    = {Implementing a fair monodic temporal logic prover},
 JOURNAL  = {AI Communications},
 VOLUME   = {23},
 NUMBER   = {2--3},
 PAGES    = {69-96},
 YEAR     = {2010},
 URL      = {http://iospress.metapress.com/content/h7262n0780p40027/fulltext.pdf},
 ABSTRACT = {Monodic first-order temporal logic is a fragment of
 first-order temporal logic for which sound and complete calculi have
 been devised. One such calculus is ordered fine-grained resolution
 with selection, which is implemented in the theorem prover
 TeMP. However, the architecture of TeMP cannot guarantee the fairness
 of its derivations. In this paper we present an architecture for a
 resolution-based monodic first-order temporal logic prover that can
 ensure fair derivations and we describe the implementation of this
 fair architecture in the theorem prover TSPASS.}
}

{"_id":"ePi5WjQ96mTCfa9Ak","bibbaseid":"ludwig-hustadt-implementingafairmonodictemporallogicprover-2010","author_short":["Ludwig, M.","Hustadt, U."],"bibdata":{"bibtype":"article","type":"article","author":[{"propositions":[],"lastnames":["Ludwig"],"firstnames":["Michel"],"suffixes":[]},{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]}],"title":"Implementing a fair monodic temporal logic prover","journal":"AI Communications","volume":"23","number":"2–3","pages":"69-96","year":"2010","url":"http://iospress.metapress.com/content/h7262n0780p40027/fulltext.pdf","abstract":"Monodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. However, the architecture of TeMP cannot guarantee the fairness of its derivations. In this paper we present an architecture for a resolution-based monodic first-order temporal logic prover that can ensure fair derivations and we describe the implementation of this fair architecture in the theorem prover TSPASS.","bibtex":"@ARTICLE{Ludwig+Hustadt@AIC2010,\n AUTHOR = {Ludwig, Michel and Hustadt, Ullrich},\n TITLE = {Implementing a fair monodic temporal logic prover},\n JOURNAL = {AI Communications},\n VOLUME = {23},\n NUMBER = {2--3},\n PAGES = {69-96},\n YEAR = {2010},\n URL = {http://iospress.metapress.com/content/h7262n0780p40027/fulltext.pdf},\n ABSTRACT = {Monodic first-order temporal logic is a fragment of\n first-order temporal logic for which sound and complete calculi have\n been devised. One such calculus is ordered fine-grained resolution\n with selection, which is implemented in the theorem prover\n TeMP. However, the architecture of TeMP cannot guarantee the fairness\n of its derivations. In this paper we present an architecture for a\n resolution-based monodic first-order temporal logic prover that can\n ensure fair derivations and we describe the implementation of this\n fair architecture in the theorem prover TSPASS.}\n}\n","author_short":["Ludwig, M.","Hustadt, U."],"key":"Ludwig+Hustadt@AIC2010","id":"Ludwig+Hustadt@AIC2010","bibbaseid":"ludwig-hustadt-implementingafairmonodictemporallogicprover-2010","role":"author","urls":{"Paper":"http://iospress.metapress.com/content/h7262n0780p40027/fulltext.pdf"},"metadata":{"authorlinks":{}},"downloads":2},"bibtype":"article","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["implementing","fair","monodic","temporal","logic","prover","ludwig","hustadt"],"title":"Implementing a fair monodic temporal logic prover","year":2010,"downloads":2}