{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T16:11:03Z","timestamp":1746115863538,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642385735"},{"type":"electronic","value":"9783642385742"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_30","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"421-435","source":"Crossref","is-referenced-by-count":0,"title":["Propositional Temporal Proving with Reductions to a SAT Problem"],"prefix":"10.1007","author":[{"given":"Richard","family":"Williams","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"30_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.3233\/AIC-2012-0523","volume":"25","author":"A. Belov","year":"2012","unstructured":"Belov, A., Lynce, I., Marques-Silva, J.: Towards efficient MUS extraction. AI Commun.\u00a025(2), 97\u2013116 (2012)","journal-title":"AI Commun."},{"key":"30_CR2","unstructured":"Biere, A.: Bounded model checking. In: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, pp. 457\u2013481. IOS Press (2009)"},{"key":"30_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: Proceedings of DATE 2007, pp. 1\u20136. IEEE (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"30_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"30_CR5","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: Proceedings of FMCAD 2012, pp. 52\u201359. IEEE (2012)"},{"key":"30_CR6","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (1999)"},{"key":"30_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-45616-3_7","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Degtyarev","year":"2002","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 85\u201399. Springer, Heidelberg (2002)"},{"issue":"1","key":"30_CR8","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A. Degtyarev","year":"2006","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Trans. Comput. Log.\u00a07(1), 108\u2013150 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Dixon, C.: Using Otter for temporal resolution. In: Advances in Temporal Logic, pp. 149\u2013166. Kluwer (2000)","DOI":"10.1007\/978-94-015-9586-5_8"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Dixon, C., Konev, B., Fisher, M., Nietiadi, S.: Deductive temporal reasoning with constraints. Journal of Applied Logic (2012)","DOI":"10.1016\/j.jal.2012.07.001"},{"issue":"1","key":"30_CR11","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":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-01702-5_7","volume-title":"Hardware and Software: Verification and Testing","author":"D. Fisman","year":"2009","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.Y.: A framework for inherent vacuity. In: Chockler, H., Hu, A.J. (eds.) HVC 2008. LNCS, vol.\u00a05394, pp. 7\u201322. Springer, Heidelberg (2009)"},{"issue":"2","key":"30_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1023\/A:1015071400913","volume":"28","author":"E. Giunchiglia","year":"2002","unstructured":"Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Autom. Reasoning\u00a028(2), 143\u2013171 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"30_CR14","unstructured":"Giunchiglia, F., Sebastiani, R.: A SAT-based decision procedure for ALC. In: Proceedings of KR 1996, pp. 304\u2013314. Morgan Kaufmann (1996)"},{"issue":"3","key":"30_CR15","doi-asserted-by":"publisher","first-page":"674","DOI":"10.1137\/S0097539797320906","volume":"33","author":"J.Y. Halpern","year":"2004","unstructured":"Halpern, J.Y., van der Meyden, R., Vardi, M.Y.: Complete axiomatizations for reasoning about knowledge and time. SIAM J. Comput.\u00a033(3), 674\u2013703 (2004)","journal-title":"SIAM J. Comput."},{"issue":"4","key":"30_CR16","doi-asserted-by":"crossref","first-page":"415","DOI":"10.3233\/FUN-2007-80404","volume":"80","author":"C. H\u00e9bert","year":"2007","unstructured":"H\u00e9bert, C., Bretto, A., Cr\u00e9milleux, B.: A data mining formalization to improve hypergraph minimal transversal computation. Fundamenta Informaticae\u00a080(4), 415\u2013433 (2007)","journal-title":"Fundamenta Informaticae"},{"key":"30_CR17","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":"30_CR18","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Proceedings of KR 2002, pp. 533\u2013546. Morgan Kaufmann (2002)"},{"issue":"1","key":"30_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-007-9084-z","volume":"40","author":"M.H. Liffiton","year":"2008","unstructured":"Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning\u00a040(1), 1\u201333 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992)","DOI":"10.1007\/978-1-4612-0931-7"},{"issue":"1-3","key":"30_CR21","first-page":"163","volume":"19","author":"J. Marques-Silva","year":"2012","unstructured":"Marques-Silva, J.: Computing minimally unsatisfiable subformulas: State of the art and future directions. Multiple-Valued Logic and Soft Computing\u00a019(1-3), 163\u2013183 (2012)","journal-title":"Multiple-Valued Logic and Soft Computing"},{"key":"30_CR22","unstructured":"Murakami, K., Uno, T.: Efficient algorithms for dualizing large-scale hypergraphs. CoRR abs\/1102.3813 (2011)"},{"key":"30_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings POPL 1989, pp. 179\u2013190. ACM (1989)","DOI":"10.1145\/75277.75293"},{"issue":"2","key":"30_CR24","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"K. Rozier","year":"2010","unstructured":"Rozier, K., Vardi, M.: LTL satisfiability checking. International Journal on Software Tools for Technology Transfer\u00a012(2), 123\u2013137 (2010)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-642-24372-1_28","volume-title":"Automated Technology for Verification and Analysis","author":"V. Schuppan","year":"2011","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol.\u00a06996, pp. 397\u2013413. Springer, Heidelberg (2011)"},{"key":"30_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/978-3-642-31365-3_42","volume-title":"Automated Reasoning","author":"M. Suda","year":"2012","unstructured":"Suda, M., Weidenbach, C.: A PLTL-prover based on labelled superposition with partial model guidance. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 537\u2013543. Springer, Heidelberg (2012)"},{"key":"30_CR27","unstructured":"Tansel, A.U., Clifford, J., Gadia, S.K., Jajodia, S., Segev, A., Snodgrass, R.T.: Temporal Databases: Theory, Design, and Implementation. Benjamin\/Cummings (1993)"},{"issue":"2","key":"30_CR28","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer and System Sciences\u00a032(2), 183\u2013219 (1986)","journal-title":"Journal of Computer and System Sciences"},{"key":"30_CR29","unstructured":"Williams, R., Konev, B.: Simplified temporal resolution using SAT solvers. In: Proceedings of ARW 2012, pp. 9\u201310. The University of Manchester (2012)"},{"key":"30_CR30","first-page":"119","volume":"28","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: An overview. Logique et Analyse\u00a028, 119\u2013152 (1985)","journal-title":"Logique et Analyse"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T11:47:40Z","timestamp":1746013660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}