{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:20:43Z","timestamp":1781076043597,"version":"3.54.1"},"reference-count":69,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,4,27]],"date-time":"2014-04-27T00:00:00Z","timestamp":1398556800000},"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":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10703-014-0208-x","type":"journal-article","created":{"date-parts":[[2014,4,26]],"date-time":"2014-04-26T15:26:12Z","timestamp":1398525972000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Resolution proof transformation for compression and interpolation"],"prefix":"10.1007","volume":"45","author":[{"given":"Simone Fulvio","family":"Rollini","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natasha","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aliaksei","family":"Tsitovich","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2014,4,27]]},"reference":[{"key":"208_CR1","volume-title":"Solvable cases of the decision problem. Studies in logic and the foundations of mathematics","author":"W Ackermann","year":"1954","unstructured":"Ackermann W (1954) Solvable cases of the decision problem. Studies in logic and the foundations of mathematics. North-Holland, Amsterdam"},{"key":"208_CR2","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2007.05.025","volume":"185","author":"H Amjad","year":"2007","unstructured":"Amjad H (2007) Compressing propositional refutations. Electron Notes Theor Comput Sci 185:3\u201315","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"3\u20134","key":"208_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s10817-008-9109-2","volume":"41","author":"H Amjad","year":"2008","unstructured":"Amjad H (2008) Data compression for proof replay. J Autom Reason 41(3\u20134):193\u2013218","journal-title":"J Autom Reason"},{"key":"208_CR4","unstructured":"Amla N, McMillan K (2003) Automatic abstraction without counterexamples. In: TACAS, pp 2\u201317"},{"key":"208_CR5","unstructured":"Bar-Ilan O, Fuhrmann O, Hoory S, Shacham O, Strichman O (2008) Linear-time reductions of resolution proofs. In: HVC, pp 114\u2013128"},{"key":"208_CR6","doi-asserted-by":"crossref","unstructured":"Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: LPAR, pp 512\u2013526","DOI":"10.1007\/11916277_35"},{"key":"208_CR7","doi-asserted-by":"crossref","unstructured":"Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule M, van Maaren H, Walsh T (eds) Handbook of satisfiability. IOS Press, Amsterdam, pp 825\u2013885","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"208_CR8","unstructured":"Bayardo RJ, Schrag R (1997) Using CSP look-back techniques to solve real-world SAT instances. In: AAAI\/IAAI, pp 203\u2013208"},{"key":"208_CR9","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. Adv Comput 58:117\u2013148","journal-title":"Adv Comput"},{"key":"208_CR10","doi-asserted-by":"crossref","unstructured":"Bofill M, Nieuwenhuis R, Oliveras A, Rodrguez-Carbonell E, Rubio A (2008) A write-based solver for SAT modulo the theory of arrays. In: FMCAD, pp 101\u2013108","DOI":"10.1109\/FMCAD.2008.ECP.18"},{"key":"208_CR11","doi-asserted-by":"crossref","unstructured":"Boudou J, Paleo B (2013) Compression of propositional resolution proofs by lowering subproofs. In: TABLEAUX, pp 237\u2013251","DOI":"10.1007\/978-3-642-40537-2_7"},{"key":"208_CR12","doi-asserted-by":"crossref","unstructured":"Bozzano M, Bruttomesso R, Cimatti A, Junttila T, Ranise S, van Rossum P, Sebastiani R (2005) Efficient satisfiability modulo theories via delayed theory combination. In: CAV, pp 335\u2013349","DOI":"10.1007\/11513988_34"},{"key":"208_CR13","doi-asserted-by":"crossref","unstructured":"Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI, pp 70\u201387","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"208_CR14","doi-asserted-by":"crossref","unstructured":"Brummayer R, Biere A (2008) Lemmas on demand for the extensional theory of arrays. In: Workshop on SMT","DOI":"10.1145\/1512464.1512467"},{"issue":"2","key":"208_CR15","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0166-218X(02)00399-2","volume":"130","author":"R Bruni","year":"2003","unstructured":"Bruni R (2003) Approximating minimal unsatisfiable subformulae by means of adaptive core search. Discret Appl Math 130(2):85\u2013100","journal-title":"Discret Appl Math"},{"key":"208_CR16","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT Solver. In: TACAS, pp 150\u2013153","DOI":"10.1007\/978-3-642-12002-2_12"},{"key":"208_CR17","doi-asserted-by":"crossref","unstructured":"Bruttomesso R, Rollini S, Sharygina N, Tsitovich A (2010) Flexible interpolation with local proof transformations. In: ICCAD, pp 770\u2013777","DOI":"10.1109\/ICCAD.2010.5654297"},{"key":"208_CR18","doi-asserted-by":"crossref","unstructured":"Christ J, Hoenicke J, Nutz A (2013) Proof tree preserving interpolation. In: TACAS, pp 124\u2013138","DOI":"10.1007\/978-3-642-36742-7_9"},{"key":"208_CR19","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Sebastiani R (2007) A simple and flexible way of computing small unsatisfiable cores in SAT modulo theories. In: SAT, pp 334\u2013339","DOI":"10.1007\/978-3-540-72788-0_32"},{"key":"208_CR20","doi-asserted-by":"crossref","unstructured":"Cimatti A, Griggio A, Sebastiani R (2008) Efficient interpolant generation in satisfiability modulo theories. In: TACAS, pp 397\u2013412","DOI":"10.1007\/978-3-540-78800-3_30"},{"key":"208_CR21","doi-asserted-by":"crossref","unstructured":"Cotton S (2010) Two techniques for minimizing resolution proofs. In: SAT, pp 306\u2013312","DOI":"10.1007\/978-3-642-14186-7_26"},{"key":"208_CR22","unstructured":"CMU Benchmarks. http:\/\/www.cs.cmu.edu\/~modelcheck\/bmc\/bmc-benchmarks.html . Accessed 24 April 2014"},{"issue":"3","key":"208_CR23","doi-asserted-by":"crossref","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig W (1957) Three uses of the herbrand\u2013gentzen theorem in relating model theory and proof theory. J Symb Log 22(3):269\u2013285","journal-title":"J Symb Log"},{"key":"208_CR24","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2009) Generalized, efficient array decision procedures. In: FMCAD, pp 45\u201352","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"208_CR25","unstructured":"de Moura L, Rue H (2002) Lemmas on demand for satisfiability solvers. In: SAT, pp 244\u2013251"},{"key":"208_CR26","doi-asserted-by":"crossref","unstructured":"Dershowitz N, Hanna Z, Nadel A (2006) A scalable algorithm for minimal unsatisfiable core extraction. In: SAT, pp 36\u201341","DOI":"10.1007\/11814948_5"},{"key":"208_CR27","unstructured":"D\u2019Silva V, Kroening D, Purandare M, Weissenbacher G (2008) Restructuring resolution refutations for interpolation. Technical report, ETH"},{"key":"208_CR28","doi-asserted-by":"crossref","unstructured":"D\u2019Silva V, Kroening D, Purandare M, Weissenbacher G (2010) Interpolant strength. In: VMCAI, pp 129\u2013145","DOI":"10.1007\/978-3-642-11319-2_12"},{"key":"208_CR29","doi-asserted-by":"crossref","unstructured":"Fontaine P, Marion J, Merz S, Nieto L, Tiu A (2006) Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: TACAS, pp 167\u2013181","DOI":"10.1007\/11691372_11"},{"key":"208_CR30","doi-asserted-by":"crossref","unstructured":"Fontaine P, Merz S, Paleo B (2011) Compression of propositional resolution proofs via partial regularization. In: CADE, pp 237\u2013251","DOI":"10.1007\/978-3-642-22438-6_19"},{"issue":"1","key":"208_CR31","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen G (1935) Untersuchungen \u00fcber das logische schlie\u00dfen. i. Math Z 39(1):176\u2013210","journal-title":"Math Z"},{"key":"208_CR32","doi-asserted-by":"crossref","unstructured":"Goel A, Krsti\u0107 S, Fuchs A (2008) Deciding array formulas with frugal axiom Instantiation. In: SMT, pp 12\u201317","DOI":"10.1145\/1512464.1512468"},{"key":"208_CR33","doi-asserted-by":"crossref","unstructured":"Goel A, Krsti\u0107 S, Tinelli C (2009) Ground interpolation for combined theories. In: CADE, pp 183\u2013198","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"208_CR34","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2003) Verification of proofs of unsatisfiability for CNF formulas. In: DATE, pp 10,886\u201310,891","DOI":"10.1109\/DATE.2003.1253718"},{"key":"208_CR35","doi-asserted-by":"crossref","unstructured":"Gomes C, Kautz H, Sabharwal A, Selman B (2008) Satisfiability solvers. In: van Harmelen F, Lifschitz V, Porter B (eds) Handbook of knowledge representation. Elsevier, Amsterdam, pp 89\u2013134","DOI":"10.1016\/S1574-6526(07)03002-7"},{"issue":"3","key":"208_CR36","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/s10601-007-9019-7","volume":"12","author":"E Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire E, Mazure B, Piette C (2007) Local-search extraction of muses. Constraints 12(3):325\u2013344","journal-title":"Constraints"},{"key":"208_CR37","doi-asserted-by":"crossref","unstructured":"Grumberg O, Lerda F, Ofer OS, Theobald M (2005) Proof-guided underapproximation-widening for multi-process systems. In: POPL, pp 122\u2013131","DOI":"10.1145\/1040305.1040316"},{"key":"208_CR38","unstructured":"Gupta A (2012) Improved single pass algorithms for resolution proof reduction. In: ATVA, pp 107\u2013121"},{"key":"208_CR39","doi-asserted-by":"crossref","unstructured":"Henzinger T, Jhala R, Majumdar R, McMillan K (2004) Abstractions from proofs. In: POPL, pp 232\u2013244","DOI":"10.1145\/964001.964021"},{"key":"208_CR40","doi-asserted-by":"crossref","unstructured":"Heule M, Hunt W, Wetzler N (2013) Trimming while checking clausal proofs. In: FMCAD","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"208_CR41","doi-asserted-by":"crossref","unstructured":"Huang J (2005) Mup: a minimal unsatisfiability prover. In: ASP-DAC, pp 432\u2013437","DOI":"10.1145\/1120725.1120907"},{"key":"208_CR42","doi-asserted-by":"crossref","unstructured":"Jhala R, McMillan K (2005) Interpolant-based transition relation approximation. In: CAV, pp 39\u201351","DOI":"10.1007\/11513988_6"},{"issue":"2","key":"208_CR43","doi-asserted-by":"crossref","first-page":"457","DOI":"10.2307\/2275541","volume":"62","author":"J Kraj\u00ed\u010dek","year":"1997","unstructured":"Kraj\u00ed\u010dek J (1997) Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J Symb Log 62(2):457\u2013486","journal-title":"J Symb Log"},{"key":"208_CR44","unstructured":"Lynce I, Marques-Silva J (2004) On computing minimum unsatisfiable cores. In: SAT, pp 305\u2013310"},{"key":"208_CR45","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Sakallah K (1996) GRASP\u2014a new search algorithm for satisfiability. In: ICCAD, pp 220\u2013227","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"208_CR46","doi-asserted-by":"crossref","unstructured":"McMillan K (2003) Interpolation and SAT-based model checking. In: CAV, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"208_CR47","doi-asserted-by":"crossref","unstructured":"McMillan K (2004) An interpolating theorem prover. In: TACAS, pp 16\u201330","DOI":"10.1007\/978-3-540-24730-2_2"},{"key":"208_CR48","doi-asserted-by":"crossref","unstructured":"McMillan K (2004) Applications of Craig interpolation to model checking. In: CSL, pp 22\u201323","DOI":"10.1007\/978-3-540-30124-0_3"},{"key":"208_CR49","doi-asserted-by":"crossref","unstructured":"Mneimneh M, Lynce I, Andraus Z, Marques-Silva J, Sakallah K (2005) A branch-and-bound algorithm for extracting smallest minimal unsatisfiable formulas. In: SAT, pp 467\u2013474","DOI":"10.1007\/11499107_40"},{"key":"208_CR50","doi-asserted-by":"crossref","unstructured":"Necula G (1997) Proof-carrying code. In: POPL, pp 106\u2013119","DOI":"10.1145\/263699.263712"},{"issue":"2","key":"208_CR51","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen D (1979) Simplification by cooperating decision procedures. ACM Trans Progr Lang Syst 1(2):245\u2013257","journal-title":"ACM Trans Progr Lang Syst"},{"key":"208_CR52","doi-asserted-by":"crossref","unstructured":"Oh Y, Mneimneh MN, Andraus ZS, Sakallah KA, Markov IL (2004) AMUSE: a minimally-unsatisfiable subformula extractor. In: DAC, pp 518\u2013523","DOI":"10.1145\/996566.996710"},{"issue":"3","key":"208_CR53","doi-asserted-by":"crossref","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k P (1997) Lower bounds for resolution and cutting plane proofs and monotone computations. J Symb Log 62(3):981\u2013998","journal-title":"J Symb Log"},{"key":"208_CR54","unstructured":"Ranise S, Tinelli C The satisfiability modulo theories library (SMT-LIB). http:\/\/www.smtlib.org . Accessed 24 April 2014"},{"key":"208_CR55","unstructured":"Rollini S Proof transformer and interpolator for propositional logic (PeRIPLO). http:\/\/verify.inf.usi.ch\/content\/periplo . Accessed 24 April 2014"},{"key":"208_CR56","unstructured":"Rollini S, Bruttomesso R, Sharygina N (2010) An efficient and flexible approach to resolution proof reduction. In: HVC, pp 182\u2013196"},{"key":"208_CR57","unstructured":"SAT Challenge (2012) http:\/\/baldur.iti.kit.edu\/SAT-Challenge-2012\/ . Accessed 24 April 2014"},{"key":"208_CR58","unstructured":"SATLIB Benchmark Suite http:\/\/www.cs.ubc.ca\/~hoos\/SATLIB\/benchm.html . Accessed 24 April 2014"},{"key":"208_CR59","first-page":"144","volume":"3","author":"R Sebastiani","year":"2007","unstructured":"Sebastiani R (2007) Lazy satisfiability modulo theories. JSAT 3:144\u2013224","journal-title":"JSAT"},{"key":"208_CR60","doi-asserted-by":"crossref","unstructured":"Shlyakhter I, Seater R, Jackson D, Sridharan M, Taghdir M (2003) Debugging overconstrained declarative models using unsatisfiable cores. In: ASE, pp 94\u2013105","DOI":"10.1109\/ASE.2003.1240298"},{"key":"208_CR61","doi-asserted-by":"crossref","unstructured":"Sinz C (2007) Compressing propositional proofs by common subproof extraction. In: EUROCAST, pp 547\u2013555","DOI":"10.1007\/978-3-540-75867-9_69"},{"issue":"1","key":"208_CR62","first-page":"75","volume":"17","author":"C Sinz","year":"2003","unstructured":"Sinz C, Kaiser A, Kuchlin W (2003) Formal methods for the validation of automotive product configuration data. AI EDAM 17(1):75\u201397","journal-title":"AI EDAM"},{"key":"208_CR63","unstructured":"Skeptik Proof Theory Library https:\/\/github.com\/Paradoxika\/Skeptik . Accessed 24 April 2014"},{"key":"208_CR64","first-page":"115","volume-title":"Studies in constructive mathematics and mathematical logic","author":"GS Tseitin","year":"1968","unstructured":"Tseitin GS (1968) On the complexity of derivation in the propositional calculus. In: Slisenko AO (ed) Studies in constructive mathematics and mathematical logic. Plenum, New York, pp 115\u2013125"},{"key":"208_CR65","doi-asserted-by":"crossref","unstructured":"Van Gelder A (2008) Verifying RUP proofs of propositional unsatisfiability. In: ISAIM","DOI":"10.1007\/978-3-540-72788-0_31"},{"issue":"1","key":"208_CR66","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1016\/j.jal.2007.07.003","volume":"7","author":"T Weber","year":"2009","unstructured":"Weber T, Amjad H (2009) Efficiently checking propositional refutations in hol theorem provers. J Appl Log 7(1):26\u201340","journal-title":"J Appl Log"},{"key":"208_CR67","doi-asserted-by":"crossref","unstructured":"Yorsh G, Musuvathi M (2005) A combination method for generating interpolants. In: CADE, pp 353\u2013368","DOI":"10.1007\/11532231_26"},{"key":"208_CR68","unstructured":"Zhang L, Malik S (2003) Extracting small unsatisfiable cores from unsatisfiable Boolean formulas. In: SAT"},{"key":"208_CR69","unstructured":"Zhang L, Sharad M (2003) Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: DATE, pp 10,880\u201310,885"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0208-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0208-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0208-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T15:31:12Z","timestamp":1746199872000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0208-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,27]]},"references-count":69,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["208"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0208-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,27]]}}}