@INCOLLECTION{HK2004,
 AUTHOR        = {Hustadt, Ullrich and Konev, Boris},
 TITLE         = {{TRP++}: A temporal resolution prover},
 BOOKTITLE     = {Collegium Logicum},
 PUBLISHER     = {Kurt G{\"o}del Society},
 YEAR          = {2004},
 EDITOR        = {Baaz, Matthias and Makowsky, Johann and Voronkov, Andrei},
 PAGES         = {65-79},
 URL           = {http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf},
 ABSTRACT      = {Temporal logics are extensions of classical logic with
 operators that deal with time. They have been used in a wide variety
 of areas within Computer Science and Artificial Intelligence, for
 example robotics, databases, hardware verification and agent-based
 systems. 
 <p>
 In particular, propositional temporal logics have been
 applied to (i) the specification and verification of reactive
 (e.g. distributed or concurrent) systems; (ii) the synthesis of
 programs from temporal specifications;; (iii) the semantics of
 executable temporal logic; (iv) algorithmic verification via
 model-checking; and (v) knowledge representation and reasoning.
 </p>
 <p>
 In developing these techniques, temporal proof is often required, and
 we base our work on practical proof techniques for the clausal
 resolution method for propositional linear-time temporal logic
 PLTL. The method is based on an intuitive clausal form, called SNF,
 comprising three main clause types and a small number of resolution
 rules.
 </p>
 While the approach has been shown to be competitive using
 a prototype implementation of the method, we now aim at an even more
 efficient implementation. This implementation, called TRP++, is the
 focus of this paper.}
}

{"_id":"pG9HQBxhQcWDp5BKK","bibbaseid":"hustadt-konev-trpatemporalresolutionprover-2004","author_short":["Hustadt, U.","Konev, B."],"bibdata":{"bibtype":"incollection","type":"incollection","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["Ullrich"],"suffixes":[]},{"propositions":[],"lastnames":["Konev"],"firstnames":["Boris"],"suffixes":[]}],"title":"TRP++: A temporal resolution prover","booktitle":"Collegium Logicum","publisher":"Kurt Gödel Society","year":"2004","editor":[{"propositions":[],"lastnames":["Baaz"],"firstnames":["Matthias"],"suffixes":[]},{"propositions":[],"lastnames":["Makowsky"],"firstnames":["Johann"],"suffixes":[]},{"propositions":[],"lastnames":["Voronkov"],"firstnames":["Andrei"],"suffixes":[]}],"pages":"65-79","url":"http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf","abstract":"Temporal logics are extensions of classical logic with operators that deal with time. They have been used in a wide variety of areas within Computer Science and Artificial Intelligence, for example robotics, databases, hardware verification and agent-based systems. <p> In particular, propositional temporal logics have been applied to (i) the specification and verification of reactive (e.g. distributed or concurrent) systems; (ii) the synthesis of programs from temporal specifications;; (iii) the semantics of executable temporal logic; (iv) algorithmic verification via model-checking; and (v) knowledge representation and reasoning. </p> <p> In developing these techniques, temporal proof is often required, and we base our work on practical proof techniques for the clausal resolution method for propositional linear-time temporal logic PLTL. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. </p> While the approach has been shown to be competitive using a prototype implementation of the method, we now aim at an even more efficient implementation. This implementation, called TRP++, is the focus of this paper.","bibtex":"@INCOLLECTION{HK2004,\n AUTHOR = {Hustadt, Ullrich and Konev, Boris},\n TITLE = {{TRP++}: A temporal resolution prover},\n BOOKTITLE = {Collegium Logicum},\n PUBLISHER = {Kurt G{\\\"o}del Society},\n YEAR = {2004},\n EDITOR = {Baaz, Matthias and Makowsky, Johann and Voronkov, Andrei},\n PAGES = {65-79},\n URL = {http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf},\n ABSTRACT = {Temporal logics are extensions of classical logic with\n operators that deal with time. They have been used in a wide variety\n of areas within Computer Science and Artificial Intelligence, for\n example robotics, databases, hardware verification and agent-based\n systems. \n <p>\n In particular, propositional temporal logics have been\n applied to (i) the specification and verification of reactive\n (e.g. distributed or concurrent) systems; (ii) the synthesis of\n programs from temporal specifications;; (iii) the semantics of\n executable temporal logic; (iv) algorithmic verification via\n model-checking; and (v) knowledge representation and reasoning.\n </p>\n <p>\n In developing these techniques, temporal proof is often required, and\n we base our work on practical proof techniques for the clausal\n resolution method for propositional linear-time temporal logic\n PLTL. The method is based on an intuitive clausal form, called SNF,\n comprising three main clause types and a small number of resolution\n rules.\n </p>\n While the approach has been shown to be competitive using\n a prototype implementation of the method, we now aim at an even more\n efficient implementation. This implementation, called TRP++, is the\n focus of this paper.}\n}\n","author_short":["Hustadt, U.","Konev, B."],"editor_short":["Baaz, M.","Makowsky, J.","Voronkov, A."],"key":"HK2004","id":"HK2004","bibbaseid":"hustadt-konev-trpatemporalresolutionprover-2004","role":"author","urls":{"Paper":"http://www.csc.liv.ac.uk/~ullrich/publications/HK_KGS.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj"],"keywords":[],"search_terms":["trp","temporal","resolution","prover","hustadt","konev"],"title":"TRP++: A temporal resolution prover","year":2004}