{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T15:55:44Z","timestamp":1726847744449},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540223450"},{"type":"electronic","value":"9783540259848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-25984-8_23","type":"book-chapter","created":{"date-parts":[[2010,9,11]],"date-time":"2010-09-11T02:31:38Z","timestamp":1284172298000},"page":"326-330","source":"Crossref","is-referenced-by-count":17,"title":["TeMP: A Temporal Monodic Prover"],"prefix":"10.1007","author":[{"given":"Ullrich","family":"Hustadt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Riazanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/3-540-45757-7_9","volume-title":"Logics in Artificial Intelligence","author":"A. Artale","year":"2002","unstructured":"Artale, A., Franconi, E., Wolter, F., Zakharyaschev, M.: A temporal description logic for reasoning over conceptual schemas and queries. In: Flesca, S., Greco, S., Leone, N., Ianni, G. (eds.) JELIA 2002. LNCS (LNAI), vol.\u00a02424, pp. 98\u2013110. Springer, Heidelberg (2002)"},{"key":"23_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"issue":"1","key":"23_CR3","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1145\/371282.371311","volume":"2","author":"M. Fisher","year":"2001","unstructured":"Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic\u00a02(1), 12\u201356 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"23_CR4","unstructured":"Fisher, M., Lisitsa, A.: Temporal verification of monodic abstract state machines. Technical Report ULCS-03-011, Department of Computer Science, University of Liverpool (2003)"},{"key":"23_CR5","first-page":"460","volume-title":"Proc. FLAIRS 2003","author":"D. Gabelaia","year":"2003","unstructured":"Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., Zakharyaschev, M.: On the computational complexity of spatio-temporal logics. In: Proc. FLAIRS 2003, pp. 460\u2013464. AAAI Press, Menlo Park (2003)"},{"key":"23_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-45085-6_21","volume-title":"Automated Deduction \u2013 CADE-19","author":"U. Hustadt","year":"2003","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: A temporal resolution prover. In: Baader, F. (ed.) CADE 2003. LNCS(LNAI), vol.\u00a02741, pp. 274\u2013278. Springer, Heidelberg (2003)"},{"key":"23_CR7","first-page":"533","volume-title":"Proc. KR 2002","author":"U. Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Proc. KR 2002, pp. 533\u2013544. Morgan Kaufmann, San Francisco (2002)"},{"key":"23_CR8","unstructured":"Janssen, G.: Logics for Digital Circuit Verification: Theory, Algorithms, and Applications. PhD thesis, Eindhoven University of Technology, The Netherlands (1999)"},{"key":"23_CR9","unstructured":"Konev, B., Degtyarev, A., Dixon, C., Fisher, M., Hustadt, U.: Mechanising first-order temporal resolution. Technical Report ULCS-03-023, University of Liverpool, Department of Computer Science (2003), \n                    \n                      http:\/\/www.csc.liv.ac.uk\/research\/"},{"issue":"1","key":"23_CR10","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1023\/B:STUD.0000027468.28935.6d","volume":"76","author":"R. Kontchakov","year":"2004","unstructured":"Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporalising tableaux. Studia Logica\u00a076(1), 91\u2013134 (2004)","journal-title":"Studia Logica"},{"issue":"2-3","key":"23_CR11","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"23_CR12","unstructured":"Schwendimann, S.: Aspects of Computational Logic. PhD thesis, Universit\u00e4t Bern, Switzerland (1998)"},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1016\/S0168-0072(01)00124-5","volume":"118","author":"F. Wolter","year":"2002","unstructured":"Wolter, F., Zakharyaschev, M.: Axiomatizing the monodic fragment of first-order temporal logic. Annals of Pure and Applied logic\u00a0118, 133\u2013145 (2002)","journal-title":"Annals of Pure and Applied logic"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-25984-8_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:21:22Z","timestamp":1620012082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-25984-8_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540223450","9783540259848"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-25984-8_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}