TRP++: A temporal resolution prover. Hustadt, U. & Konev, B. In Baaz, M., Makowsky, J., & Voronkov, A., editors, *Collegium Logicum*, pages 65-79. Kurt Gödel Society, 2004. Paper abstract bibtex 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.

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.

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.

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.

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

Downloads: 0

{"_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}