{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:28:25Z","timestamp":1746289705692},"reference-count":99,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2015,5,31]],"date-time":"2015-05-31T00:00:00Z","timestamp":1433030400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,4]]},"DOI":"10.1007\/s00236-015-0242-1","type":"journal-article","created":{"date-parts":[[2015,5,30]],"date-time":"2015-05-30T06:14:56Z","timestamp":1432966496000},"page":"247-299","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Extracting unsatisfiable cores for LTL via temporal resolution"],"prefix":"10.1007","volume":"53","author":[{"given":"Viktor","family":"Schuppan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,5,31]]},"reference":[{"key":"242_CR1","doi-asserted-by":"crossref","unstructured":"Amjad, H.: Compressing propositional refutations. In: Merz, S., Nipkow, T. (eds.) AVoCS, Elsevier, Electr. Notes Theor. Comput. Sci., vol. 185, pp. 3\u201315 (2006)","DOI":"10.1016\/j.entcs.2007.05.025"},{"key":"242_CR2","doi-asserted-by":"crossref","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.: Enhanced vacuity detection in linear temporal logic. In: Hunt. Jr., W., Somenzi, F. (eds.) CAV, Springer, LNCS, vol. 2725, pp. 368\u2013380 (2003)","DOI":"10.1007\/978-3-540-45069-6_35"},{"issue":"8","key":"242_CR3","doi-asserted-by":"crossref","first-page":"714","DOI":"10.1016\/j.is.2012.05.001","volume":"37","author":"A Awad","year":"2012","unstructured":"Awad, A., Gor\u00e9, R., Hou, Z., Thomson, J., Weidlich, M.: An iterative approach to synthesize business process templates from compliance rules. Inf. Syst. 37(8), 714\u2013736 (2012)","journal-title":"Inf. Syst."},{"key":"242_CR4","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","year":"2007","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2007)"},{"key":"242_CR5","doi-asserted-by":"crossref","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, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 19\u201399. Elsevier and MIT Press, Amsterdam and Cambridge (2001)"},{"key":"242_CR6","unstructured":"Bakker, R., Dikker, F., Tempelman, F., Wognum, P.: Diagnosing and solving over-determined constraint satisfaction problems. In: IJCAI, pp. 276\u2013281 (1993)"},{"key":"242_CR7","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"242_CR8","doi-asserted-by":"crossref","unstructured":"Beatty, D., Bryant, R.: Formally verifying a microprocessor using a simulation methodology. In: DAC, pp. 596\u2013602 (1994)","DOI":"10.1145\/196244.196575"},{"issue":"2","key":"242_CR9","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in temporal model checking. Form. Methods Syst. Des. 18(2), 141\u2013163 (2001)","journal-title":"Form. Methods Syst. Des."},{"issue":"4","key":"242_CR10","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1108\/17563780911005818","volume":"2","author":"A Behdenna","year":"2009","unstructured":"Behdenna, A., Dixon, C., Fisher, M.: Deductive verification of simple foraging robotic behaviours. Int. J. Intell. Comput. Cybern. 2(4), 604\u2013643 (2009)","journal-title":"Int. J. Intell. Comput. Cybern."},{"key":"242_CR11","doi-asserted-by":"crossref","unstructured":"Belov, A., Marques Silva, J.: Minimally unsatisfiable Boolean circuits. In: Sakallah, K., Simon, L. (eds.) SAT, Springer, LNCS, vol. 6695, pp. 145\u2013158 (2011)","DOI":"10.1007\/978-3-642-21581-0_13"},{"key":"242_CR12","first-page":"457","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"A Biere","year":"2009","unstructured":"Biere, A.: Bounded model checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457\u2013481. IOS Press, Amsterdam (2009)"},{"key":"242_CR13","doi-asserted-by":"crossref","unstructured":"Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), (2006)","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"242_CR14","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. In: Glesner, S., Knoop, J., Drechsler, R. (eds.) COCV, Elsevier, Electr. Notes Theor. Comput. Sci., vol. 190(4), pp. 3\u201316 (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"242_CR15","doi-asserted-by":"crossref","unstructured":"Bruni, R., Sassano, A.: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In: Kautz H, Selman B (eds.) SAT, Elsevier, Electronic Notes in Discrete Mathematics, vol. 9, pp. 162\u2013173 (2001)","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"242_CR16","first-page":"339","volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","author":"HK B\u00fcning","year":"2009","unstructured":"B\u00fcning, H.K., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339\u2013401. IOS Press, Amsterdam (2009)"},{"issue":"2","key":"242_CR17","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"242_CR18","doi-asserted-by":"crossref","unstructured":"Chiappini, A., Cimatti, A., Macchi, L., Rebollo, O., Roveri, M., Susi, A., Tonetta, S., Vittorini, B.: Formalization and validation of a subset of the European Train Control System. In: Kramer, J., Bishop, J., Devanbu, P., Uchitel, S. (eds.) ICSE (2), ACM, pp. 109\u2013118 (2010)","DOI":"10.1145\/1810295.1810312"},{"issue":"2","key":"242_CR19","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J Chinneck","year":"1991","unstructured":"Chinneck, J., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. INFORMS J. Comput. 3(2), 157\u2013168 (1991)","journal-title":"INFORMS J. Comput."},{"key":"242_CR20","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K. (eds.) CAV, Springer, LNCS, vol. 2404, pp. 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"242_CR21","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tonetta, S.: Boolean abstraction for temporal logic satisfiability. In: Damm, W., Hermanns, H. (eds.) CAV, Springer, LNCS, vol. 4590, pp. 532\u2013546 (2007)","DOI":"10.1007\/978-3-540-73368-3_53"},{"key":"242_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Roveri, M., Schuppan, V., Tchaltsev, A.: Diagnostic information for realizability. In: Logozzo, F., Peled, D., Zuck, L. (eds.) VMCAI, Springer, LNCS, vol. 4905, pp. 52\u201367 (2008)","DOI":"10.1007\/978-3-540-78163-9_9"},{"key":"242_CR23","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1613\/jair.3196","volume":"40","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. (JAIR) 40, 701\u2013728 (2011)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"242_CR24","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: Proving and explaining the unfeasibility of message sequence charts for hybrid systems. In: Bjesse, P., Slobodov\u00e1, A. (eds.) FMCAD, FMCAD Inc., pp. 54\u201362 (2011)"},{"issue":"1","key":"242_CR25","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1023\/A:1008615614281","volume":"10","author":"E Clarke","year":"1997","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. Form. Methods Syst. Des. 10(1), 47\u201371 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"242_CR26","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"242_CR27","doi-asserted-by":"crossref","unstructured":"Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT, Springer, LNCS, vol. 2919, pp. 78\u201392 (2003)","DOI":"10.1007\/978-3-540-24605-3_7"},{"key":"242_CR28","doi-asserted-by":"crossref","unstructured":"De Wulf, M., Doyen, L., Maquet, N., Raskin, J.: Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Ramakrishnan, C., Rehof, J. (eds.) TACAS, Springer, LNCS, vol. 4963, pp. 63\u201377 (2008)","DOI":"10.1007\/978-3-540-78800-3_6"},{"issue":"1","key":"242_CR29","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1006\/inco.2001.3094","volume":"174","author":"S Demri","year":"2002","unstructured":"Demri, S., Schnoebelen, P.: The complexity of propositional linear temporal logics in simple cases. Inf. Comput. 174(1), 84\u2013103 (2002)","journal-title":"Inf. Comput."},{"key":"242_CR30","unstructured":"Dixon, C.: Strategies for temporal resolution. PhD thesis, Department of Computer Science, University of Manchester. http:\/\/apt.cs.manchester.ac.uk\/ftp\/pub\/TR\/UMCS-95-12-1.ps.Z (1995)"},{"key":"242_CR31","unstructured":"Dixon, C.: Using Otter for temporal resolution. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds.) ICTL, Springer, Applied Logic Series, vol. 16, pp. 149\u2013166 (1997)"},{"issue":"1\u20132","key":"242_CR32","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1023\/A:1018942108420","volume":"22","author":"C Dixon","year":"1998","unstructured":"Dixon, C.: Temporal resolution using a breadth-first search algorithm. Ann. Math. Artif. Intell. 22(1\u20132), 87\u2013115 (1998)","journal-title":"Ann. Math. Artif. Intell."},{"key":"242_CR33","doi-asserted-by":"crossref","unstructured":"D\u2019Silva, V., Kroening, D., Purandare, M., Weissenbacher, G.: Interpolant strength. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI, Springer, LNCS, vol. 5944, pp. 129\u2013145 (2010)","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"242_CR34","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, Berlin (2006)"},{"key":"242_CR35","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics","author":"E Emerson","year":"1990","unstructured":"Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pp. 995\u20131072. Elsevier and MIT Press, Amsterdam and Cambridge (1990)"},{"key":"242_CR36","unstructured":"Fisher, M.: A resolution method for temporal logic. In: IJCAI, pp. 99\u2013104 (1991)"},{"key":"242_CR37","unstructured":"Fisher, M., No\u00ebl, P.: Transformation and synthesis in MetateM. Part I: propositional MetateM. Tech. Rep. UMCS-92-2-1, University of Manchester, Department of Computer Science. http:\/\/apt.cs.manchester.ac.uk\/ftp\/pub\/TR\/UMCS-92-2-1.ps.Z (1992)"},{"issue":"1","key":"242_CR38","doi-asserted-by":"crossref","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 Trans. Comput. Log. 2(1), 12\u201356 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"242_CR39","doi-asserted-by":"crossref","unstructured":"Fisman, D., Kupferman, O., Sheinvald-Faragy, S., Vardi, M.: A framework for inherent vacuity. In: Chockler, H., Hu, A. (eds.) HVC, Springer, LNCS, vol. 5394, pp. 7\u201322 (2008)","DOI":"10.1007\/978-3-642-01702-5_7"},{"key":"242_CR40","unstructured":"Gheorghiu, M., Gurfinkel, A.: VaqUoT: A tool for vacuity detection. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM, Springer, LNCS, vol. 4085, tool presentation. http:\/\/fm06.mcmaster.ca\/VaqUoT.pdf (2006)"},{"key":"242_CR41","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: DATE, IEEE Computer Society, pp. 10886\u201310891 (2003)","DOI":"10.1109\/DATE.2003.1253718"},{"key":"242_CR42","unstructured":"Gor\u00e9, R., Huang, J., Sergeant, T., Thomson, J.: Finding Minimal Unsatisfiable Subsets in Linear Temporal Logic using BDDs. http:\/\/www.timsergeant.com\/files\/pltlmup\/gore_huang_sergeant_thomson_mus_pltl.pdf (2013)"},{"key":"242_CR43","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Chechik, M.: How vacuous is vacuous? In: Jensen, K., Podelski, A. (eds.) TACAS, Springer, LNCS, vol. 2988, pp. 451\u2013466 (2004)","DOI":"10.1007\/978-3-540-24730-2_34"},{"key":"242_CR44","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0304-3975(83)90097-X","volume":"27","author":"J Halpern","year":"1983","unstructured":"Halpern, J., Reif, J.: The propositional dynamic logic of deterministic, well-structured programs. Theor. Comput. Sci. 27, 127\u2013165 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"242_CR45","doi-asserted-by":"crossref","unstructured":"Hantry, F., Hacid, M.: Handling conflicts in depth-first search for LTL tableau to debug compliance based languages. In: Pimentel, E., Valero, V. (eds.) FLACOS, EPTCS, vol. 68, pp. 39\u201353 (2011)","DOI":"10.4204\/EPTCS.68.5"},{"key":"242_CR46","unstructured":"Hantry, F., Sa\u00efs, L., Hacid, M.: On the complexity of computing minimal unsatisfiable LTL formulas. Electron. Colloq. Comput. Complex. (ECCC) 19(69), (2012)"},{"key":"242_CR47","unstructured":"Harding, A.: Symbolic strategy synthesis for games with LTL winning conditions. PhD thesis, University of Birmingham (2005)"},{"key":"242_CR48","doi-asserted-by":"crossref","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, S., Seyfried, M.: Propositional logics on the computer. In: Baumgartner, P., H\u00e4hnle, R., Posegga, J. (eds.) TABLEAUX, Springer, LNCS, vol. 918, pp. 310\u2013323 (1995)","DOI":"10.1007\/3-540-59338-1_44"},{"key":"242_CR49","unstructured":"Hoos, H.: Heavy-tailed behaviour in randomised systematic search algorithms for SAT? Tech. Rep. TR-99-16, University of British Columbia, Department of Computer Science (1999)"},{"key":"242_CR50","unstructured":"Horridge, M.: Justification based explanation in ontologies. PhD thesis, School of Computer Science, Faculty of Engineering and Physical Sciences, University of Manchester. http:\/\/www.escholar.manchester.ac.uk\/uk-ac-man-scw:131699 (2011)"},{"key":"242_CR51","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1145\/1120725.1120907","volume-title":"ASP-DAC","author":"J Huang","year":"2005","unstructured":"Huang, J.: MUP: a minimal unsatisfiability prover. In: Tang, T. (ed.) ASP-DAC, pp. 432\u2013437. ACM Press, Nre York (2005)"},{"key":"242_CR52","doi-asserted-by":"crossref","unstructured":"Hustadt, U., Konev, B.: TRP++ 2.0: a temporal resolution prover. In: Baader, F. (ed.) CADE, Springer, LNCS, vol. 2741, pp. 274\u2013278 (2003)","DOI":"10.1007\/978-3-540-45085-6_21"},{"key":"242_CR53","unstructured":"Hustadt, U., Konev, B.: TRP++: a temporal resolution prover. In: Baaz, M., Makowsky, J., Voronkov, A. (eds.) Collegium Logicum, vol. 8, Kurt G\u00f6del Society, pp. 65\u201379 (2004)"},{"key":"242_CR54","unstructured":"Hustadt, U., Schmidt, R.A.: Scientific benchmarking with temporal logic decision procedures. In: Fensel, D., Giunchiglia, F., McGuinness, D., Williams, M. (eds.) KR, Morgan Kaufmann, pp. 533\u2013546 (2002)"},{"key":"242_CR55","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: FMCAD, IEEE Computer Society, pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"242_CR56","volume-title":"The C++ Standard Library: A Tutorial and Reference","author":"N Josuttis","year":"2012","unstructured":"Josuttis, N.: The C++ Standard Library: A Tutorial and Reference, 2nd edn. Addison-Wesley, Reading (2012)","edition":"2"},{"key":"242_CR57","unstructured":"Junker, U.: QuickXplain: conflict detection for arbitrary constraint propagation algorithms. In: CONS. http:\/\/www.lirmm.fr\/~bessiere\/ws_ijcai01\/junker.ps.gz (2001)"},{"key":"242_CR58","doi-asserted-by":"crossref","unstructured":"Jussila, T., Sinz, C., Biere, A.: Extended resolution proofs for symbolic SAT solving with quantification. In: Biere, A., Gomes, C. (eds.) SAT, Springer, LNCS, vol. 4121, pp. 54\u201360 (2006)","DOI":"10.1007\/11814948_8"},{"key":"242_CR59","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.: Algorithmic verification of linear temporal logic specifications. In: Larsen, K., Skyum, S., Winskel, G. (eds.) ICALP, Springer, LNCS, vol. 1443, pp. 1\u201316 (1998)","DOI":"10.1007\/BFb0055036"},{"key":"242_CR60","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging formal specifications using simple counterstrategies. In: FMCAD, IEEE, pp. 152\u2013159 (2009)","DOI":"10.1109\/FMCAD.2009.5351127"},{"key":"242_CR61","doi-asserted-by":"crossref","unstructured":"K\u00f6nighofer, R., Hofferek, G., Bloem, R.: Debugging unrealizable specifications with model-based diagnosis. In: Barner, S., Harris, I., Kroening, D., Raz, O. (eds.) HVC, Springer, LNCS, vol. 6504, pp. 29\u201345 (2010)","DOI":"10.1007\/978-3-642-19583-9_8"},{"issue":"12","key":"242_CR62","doi-asserted-by":"crossref","first-page":"1343","DOI":"10.1163\/156855308X344864","volume":"22","author":"H Kress-Gazit","year":"2008","unstructured":"Kress-Gazit, H., Fainekos, G., Pappas, G.: Translating structured English to robot controllers. Adva. Rob. 22(12), 1343\u20131359 (2008)","journal-title":"Adva. Rob."},{"key":"242_CR63","doi-asserted-by":"crossref","unstructured":"Kupferman, O.: Sanity checks in formal verification. In: Baier, C., Hermanns, H. (eds.) CONCUR, Springer, LNCS, vol. 4137, pp. 37\u201351 (2006)","DOI":"10.1007\/11817949_3"},{"issue":"2","key":"242_CR64","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. STTT 4(2), 224\u2013233 (2003)","journal-title":"STTT"},{"key":"242_CR65","first-page":"97","volume-title":"POPL","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Van Deusen, M., Galil, Z., Reid, B. (eds.) POPL, pp. 97\u2013107. ACM Press, New York (1985)"},{"issue":"2\u20133","key":"242_CR66","doi-asserted-by":"crossref","first-page":"69","DOI":"10.3233\/AIC-2010-0457","volume":"23","author":"M Ludwig","year":"2010","unstructured":"Ludwig, M., Hustadt, U.: Implementing a fair monodic temporal logic prover. AI Commun. 23(2\u20133), 69\u201396 (2010)","journal-title":"AI Commun."},{"issue":"1\u20133","key":"242_CR67","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. Mult. Valued Log. Soft Comput. 19(1\u20133), 163\u2013183 (2012)","journal-title":"Mult. Valued Log. Soft Comput."},{"key":"242_CR68","unstructured":"Marques-Silva, J., Janota, M.: Computing minimal sets on propositional formulae i: problems & reductions. arXiv:1402.3011 [cs.LO] (2014)"},{"key":"242_CR69","unstructured":"Nadel, A.: Understanding and improving a modern SAT solver. PhD thesis, The Blavatnik School of Computer Science, Raymond and Beverly Sackler Faculty of Exact Sciences, Tel Aviv University. http:\/\/www.cs.tau.ac.il\/thesis\/thesis\/nadel.pdf (2009)"},{"key":"242_CR70","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D. (eds.) CAV, Springer, LNCS, vol. 3114, pp. 57\u201369 (2004)","DOI":"10.1007\/978-3-540-27813-9_5"},{"issue":"6","key":"242_CR71","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/BF01210997","volume":"7","author":"P No\u00ebl","year":"1995","unstructured":"No\u00ebl, P.: A transformation-based synthesis of temporal specifications. Form. Asp. Comput. 7(6), 587\u2013619 (1995)","journal-title":"Form. Asp. Comput."},{"key":"242_CR72","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods. Texts in Computer Science","author":"D Peled","year":"2001","unstructured":"Peled, D.: Software Reliability Methods. Texts in Computer Science. Springer, Berlin (2001)"},{"key":"242_CR73","doi-asserted-by":"crossref","unstructured":"Pesic, M., van der Aalst, W.: A declarative approach for flexible business processes management. In: Eder, J., Dustdar, S. (eds.) Business Process Management Workshops, Springer, LNCS, vol. 4103, pp. 169\u2013180 (2006)","DOI":"10.1007\/11837862_18"},{"key":"242_CR74","doi-asserted-by":"crossref","unstructured":"Pill, I., Semprini, S., Cavada, R., Roveri, M., Bloem, R., Cimatti, A.: Formal analysis of hardware requirements. In: Sentovich, E. (ed.) DAC, ACM, pp. 821\u2013826 (2006)","DOI":"10.1109\/DAC.2006.229231"},{"issue":"3","key":"242_CR75","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"key":"242_CR76","doi-asserted-by":"crossref","unstructured":"Purandare, M., Wahl, T., Kroening, D.: Strengthening properties using abstraction refinement. In: DATE, IEEE, pp. 1692\u20131697 (2009)","DOI":"10.1109\/DATE.2009.5090935"},{"key":"242_CR77","doi-asserted-by":"crossref","unstructured":"Raman, V., Kress-Gazit, H.: Analyzing unsynthesizable specifications for high-level robot behavior using LTLMoP. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, Springer, LNCS, vol. 6806, pp. 663\u2013668 (2011)","DOI":"10.1007\/978-3-642-22110-1_54"},{"issue":"1","key":"242_CR78","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10703-014-0208-x","volume":"45","author":"S Rollini","year":"2014","unstructured":"Rollini, S., Bruttomesso, R., Sharygina, N., Tsitovich, A.: Resolution proof transformation for compression and interpolation. Form. Methods Syst. Des. 45(1), 1\u201341 (2014)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"242_CR79","doi-asserted-by":"crossref","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. STTT 12(2), 123\u2013137 (2010)","journal-title":"STTT"},{"key":"242_CR80","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob, G., Walsh, T. (eds.) IJCAI, Morgan Kaufmann, pp. 355\u2013362 (2003)"},{"key":"242_CR81","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Extracting unsatisfiable cores for LTL via temporal resolution. arXiv:1212.3884v1 [cs.LO] (2012)","DOI":"10.1109\/TIME.2013.15"},{"issue":"7\u20138","key":"242_CR82","doi-asserted-by":"crossref","first-page":"908","DOI":"10.1016\/j.scico.2010.11.004","volume":"77","author":"V Schuppan","year":"2012","unstructured":"Schuppan, V.: Towards a notion of unsatisfiable and unrealizable cores for LTL. Sci. Comput. Program. 77(7\u20138), 908\u2013939 (2012)","journal-title":"Sci. Comput. Program."},{"key":"242_CR83","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Enhancing unsatisfiable cores for LTL with information on temporal relevance. In: Bortolussi, L., Wiklicky, H. (eds.) QAPL, EPTCS, vol. 117, pp. 49\u201365 (2013)","DOI":"10.4204\/EPTCS.117.4"},{"key":"242_CR84","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Extracting unsatisfiable cores for LTL via temporal resolution. In: Sanchez, C., Venable, B., Zimanyi, E. (eds.) TIME, IEEE Computer Society, pp. 54\u201361 (2013)","DOI":"10.1109\/TIME.2013.15"},{"key":"242_CR85","doi-asserted-by":"crossref","unstructured":"Schuppan, V.: Extracting unsatisfiable cores for LTL via temporal resolution (full version). arXiv:1212.3884 [cs.LO] (2015)","DOI":"10.1007\/s00236-015-0242-1"},{"key":"242_CR86","doi-asserted-by":"crossref","unstructured":"Schuppan, V., Darmawan, L.: Evaluating LTL satisfiability solvers. In: Bultan, T., Hsiung, P. (eds.) ATVA, Springer, LNCS, vol. 6996, pp. 397\u2013413 (2011)","DOI":"10.1007\/978-3-642-24372-1_28"},{"key":"242_CR87","unstructured":"Shlyakhter, I.: Declarative symbolic pure-logic model checking. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusets Institute of Technology. http:\/\/hdl.handle.net\/1721.1\/30184 (2005)"},{"key":"242_CR88","doi-asserted-by":"crossref","unstructured":"Shlyakhter, I., Seater, R., Jackson, D., Sridharan, M., Taghdiri, M.: Debugging overconstrained declarative models using unsatisfiable cores. In: ASE, IEEE Computer Society, pp. 94\u2013105 (2003)","DOI":"10.1109\/ASE.2003.1240298"},{"key":"242_CR89","series-title":"C++ in-depth series","volume-title":"The Boost Graph Library\u2014User Guide and Reference Manual","author":"J Siek","year":"2002","unstructured":"Siek, J., Lee, L., Lumsdaine, A.: The Boost Graph Library\u2014User Guide and Reference Manual. C++ in-depth series. Pearson\/Prentice Hall, Englewood Cliffs (2002)"},{"key":"242_CR90","unstructured":"Simmonds, J., Davies, J., Gurfinkel, A.: VaqTree: Efficient vacuity detection for bounded model checking. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM, Springer, LNCS, vol. 4085, tool presentation. http:\/\/fm06.mcmaster.ca\/jocelyn.pdf (2006)"},{"issue":"5","key":"242_CR91","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/s10009-009-0134-1","volume":"12","author":"J Simmonds","year":"2010","unstructured":"Simmonds, J., Davies, J., Gurfinkel, A., Chechik, M.: Exploiting resolution proofs to speed up LTL vacuity detection for BMC. STTT 12(5), 319\u2013335 (2010)","journal-title":"STTT"},{"issue":"3","key":"242_CR92","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"242_CR93","unstructured":"The VIS Group: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T. (eds.) CAV, Springer, LNCS, vol. 1102, pp. 428\u2013432 (1996)"},{"key":"242_CR94","doi-asserted-by":"crossref","unstructured":"Torlak, E., Chang, F.S.H., Jackson, D.: Finding minimal unsatisfiable cores of declarative specifications. In: Cu\u00e9llar, J., Maibaum, T., Sere, K. (eds.) FM, Springer, LNCS, vol. 5014, pp. 326\u2013341 (2008)","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"242_CR95","unstructured":"Van Gelder, A.: Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution, AI&M 24\u20132002. Seventh International Symposium on Artificial Intelligence and Mathematics, January 2\u20134, 2002, Fort Lauderdale, Florida (2002)"},{"issue":"5","key":"242_CR96","doi-asserted-by":"crossref","first-page":"1648","DOI":"10.1145\/186025.186103","volume":"16","author":"D Whalley","year":"1994","unstructured":"Whalley, D.: Automatic isolation of compiler errors. ACM Trans. Program. Lang. Syst. 16(5), 1648\u20131659 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"242_CR97","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1109\/32.988498","volume":"28","author":"A Zeller","year":"2002","unstructured":"Zeller, A., Hildebrandt, R.: Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng. 28(2), 183\u2013200 (2002)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"242_CR98","unstructured":"Zhang, L.: Searching for truth: techniques for satisfiability of Boolean formulas. PhD thesis, Department of Electrical Engineering, Princeton University (2003)"},{"key":"242_CR99","unstructured":"Zhang, L., Malik, S.: Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In: DATE, IEEE Computer Society, pp. 10880\u201310885 (2003)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0242-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0242-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0242-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,2]],"date-time":"2020-09-02T21:49:29Z","timestamp":1599083369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0242-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,31]]},"references-count":99,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["242"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0242-1","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,31]]}}}