@INPROCEEDINGS{Hustadt+Konev@CADE2003,
 AUTHOR        = {Hustadt, U. and Konev, Boris},
 YEAR          = {2003},
 TITLE         = {TRP{+}{+} 2.0:  A temporal resolution prover},
 XEDITOR       = {Baader, F.},
 BOOKTITLE     = {Proceedings of the 19th International Conference on Automated Deduction
 (CADE-19) [Miamia Beach, USA, July/August 2003]},
 SERIES        = {Lecture Notes in Artificial Intelligence},
 VOLUME        = {2741},
 PUBLISHER     = {Springer},
 PAGES         = {274-278},
 URL           = {Hustadt+Konev@CADE2003.pdf},
 ABSTRACT      = {In this paper we present TRP++ Version 2.0,
 a theorem prover for propositional linear time logic PLTL. 
 TRP++ is based on the resolution method for PLTL developed by 
 Fisher which involves the translation of PLTL-formulae to 
 separated normal form and the application of the inference rules 
 of the temporal resolution calculus.}
}

{"_id":"76ca97kXyJTSR4gLZ","bibbaseid":"hustadt-konev-trp20atemporalresolutionprover-2003","author_short":["Hustadt, U.","Konev, B."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Hustadt"],"firstnames":["U."],"suffixes":[]},{"propositions":[],"lastnames":["Konev"],"firstnames":["Boris"],"suffixes":[]}],"year":"2003","title":"TRP++ 2.0: A temporal resolution prover","xeditor":"Baader, F.","booktitle":"Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miamia Beach, USA, July/August 2003]","series":"Lecture Notes in Artificial Intelligence","volume":"2741","publisher":"Springer","pages":"274-278","url":"Hustadt+Konev@CADE2003.pdf","abstract":"In this paper we present TRP++ Version 2.0, a theorem prover for propositional linear time logic PLTL. TRP++ is based on the resolution method for PLTL developed by Fisher which involves the translation of PLTL-formulae to separated normal form and the application of the inference rules of the temporal resolution calculus.","bibtex":"@INPROCEEDINGS{Hustadt+Konev@CADE2003,\n AUTHOR = {Hustadt, U. and Konev, Boris},\n YEAR = {2003},\n TITLE = {TRP{+}{+} 2.0: A temporal resolution prover},\n XEDITOR = {Baader, F.},\n BOOKTITLE = {Proceedings of the 19th International Conference on Automated Deduction\n (CADE-19) [Miamia Beach, USA, July/August 2003]},\n SERIES = {Lecture Notes in Artificial Intelligence},\n VOLUME = {2741},\n PUBLISHER = {Springer},\n PAGES = {274-278},\n URL = {Hustadt+Konev@CADE2003.pdf},\n ABSTRACT = {In this paper we present TRP++ Version 2.0,\n a theorem prover for propositional linear time logic PLTL. \n TRP++ is based on the resolution method for PLTL developed by \n Fisher which involves the translation of PLTL-formulae to \n separated normal form and the application of the inference rules \n of the temporal resolution calculus.}\n}\n","author_short":["Hustadt, U.","Konev, B."],"key":"Hustadt+Konev@CADE2003","id":"Hustadt+Konev@CADE2003","bibbaseid":"hustadt-konev-trp20atemporalresolutionprover-2003","role":"author","urls":{"Paper":"http://cgi.csc.liv.ac.uk/~ullrich/publications/Hustadt+Konev@CADE2003.pdf"},"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"http://cgi.csc.liv.ac.uk/~ullrich/publications/all.bib?authorFirst=1","dataSources":["WhiGijHmCtTSdLaAj","FgmYE34DdKWThg2dR"],"keywords":[],"search_terms":["trp","temporal","resolution","prover","hustadt","konev"],"title":"TRP++ 2.0: A temporal resolution prover","year":2003}