{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:28Z","timestamp":1778498428549,"version":"3.51.4"},"reference-count":59,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T00:00:00Z","timestamp":1649635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"State of Upper Austria","award":["LIT AI Lab"],"award-info":[{"award-number":["LIT AI Lab"]}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P31571-N32"],"award-info":[{"award-number":["P31571-N32"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automated reasoning techniques based on computer algebra have seen renewed interest in recent years and are for example heavily used in formal verification of arithmetic circuits. However, the verification process might contain errors. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. For algebraic reasoning, two proof systems, Nullstellensatz and polynomial calculus, are available and are well-known in proof complexity. A Nullstellensatz proof captures whether a polynomial can be represented as a linear combination of a given set of polynomials by providing the co-factors of the linear combination. Proofs in polynomial calculus dynamically capture that a polynomial can be derived from a given set of polynomials using algebraic ideal theory. In this article we present the practical algebraic calculus as an instantiation of the polynomial calculus that can be checked efficiently. We further modify the practical algebraic calculus and gain LPAC (practical algebraic calculus + linear combinations) that includes linear combinations. In this way we are not only able to represent both Nullstellensatz and polynomial calculus proofs, but we are also able to blend both proof formats. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too. We demonstrate the different proof formats on the use case of arithmetic circuit verification and discuss how these proofs can be produced as a by-product in formal verification. We present the proof checkers <jats:sc>Pacheck<\/jats:sc>, <jats:sc>Past\u00e8que<\/jats:sc>, and <jats:sc>Nuss-Checker<\/jats:sc>. <jats:sc>Pacheck<\/jats:sc> checks proofs in practical algebraic calculus more efficiently than <jats:sc>Past\u00e8que<\/jats:sc>, but the latter is formally verified using the proof assistant Isabelle\/HOL. The tool <jats:sc>Nuss-Checker<\/jats:sc> is used to check proofs in the Nullstellensatz format.<\/jats:p>","DOI":"10.1007\/s10703-022-00391-x","type":"journal-article","created":{"date-parts":[[2022,4,11]],"date-time":"2022-04-11T17:30:55Z","timestamp":1649698255000},"page":"73-107","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Practical algebraic calculus and Nullstellensatz with the checkers Pacheck and Past\u00e8que and Nuss-Checker"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5645-0292","authenticated-orcid":false,"given":"Daniela","family":"Kaufmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Fleury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Kauers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,4,11]]},"reference":[{"issue":"4","key":"391_CR1","doi-asserted-by":"publisher","first-page":"1184","DOI":"10.1137\/S0097539700366735","volume":"31","author":"M Alekhnovich","year":"2002","unstructured":"Alekhnovich M, Ben-Sasson E, Razborov AA, Wigderson A (2002) Space complexity in propositional calculus. SIAM J Comput 31(4):1184\u20131211","journal-title":"SIAM J Comput"},{"issue":"1","key":"391_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1006\/jcss.1998.1575","volume":"57","author":"P Beame","year":"1998","unstructured":"Beame P, Cook SA, Edmonds J, Impagliazzo R, Pitassi T (1998) The relative complexity of NP search problems. J Comput Syst Sci 57(1):3\u201319","journal-title":"J Comput Syst Sci"},{"key":"391_CR3","doi-asserted-by":"crossref","unstructured":"Beame P, Impagliazzo R, Kraj\u00edcek J, Pitassi T, Pudl\u00e1k P (1996) Lower bounds on Hilbert\u2019s Nullstellensatz and propositional proofs. Proc London Math Soc s3\u201373:1\u201326","DOI":"10.1112\/plms\/s3-73.1.1"},{"key":"391_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0913-3","volume-title":"Gr\u00f6bner bases","author":"T Becker","year":"1993","unstructured":"Becker T, Weispfenning V, Kredel H (1993) Gr\u00f6bner bases. Springer, Berlin"},{"issue":"2","key":"391_CR5","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette JC, B\u00f6hme S, Fleury M, Smolka SJ, Steckermeier A (2016) Semi-intelligible Isar proofs from machine-generated proofs. J Autom Reasoning 56(2):155\u2013200. https:\/\/doi.org\/10.1007\/s10817-015-9335-3","journal-title":"J Autom Reasoning"},{"key":"391_CR6","doi-asserted-by":"publisher","unstructured":"Bright C, Kotsireas I, Ganesh V (04 2018) Applying computer algebra systems and SAT solvers to the Williamson conjecture. J Symb Comput. https:\/\/doi.org\/10.1016\/j.jsc.2019.07.024","DOI":"10.1016\/j.jsc.2019.07.024"},{"key":"391_CR7","unstructured":"Bright C, Kotsireas I, Ganesh V (2019) SAT solvers and computer algebra systems: a powerful combination for mathematics. CoRR arXiv:abs\/1907.04408"},{"key":"391_CR8","unstructured":"Buchberger B (1965) Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. thesis, University of Innsbruck"},{"key":"391_CR9","first-page":"233","volume":"336","author":"S Buss","year":"2021","unstructured":"Buss S, Nordstr\u00f6m J (2021) Proof complexity and sat solving. Handbook Satis 336:233\u2013350","journal-title":"Handbook Satis"},{"key":"391_CR10","doi-asserted-by":"publisher","unstructured":"Choo D, Soos M, Chai KMA, Meel KS (2019) Bosphorus: bridging ANF and CNF solvers. In: Teich J, Fummi F (eds) DATE 2019. IEEE, pp. 468\u2013473. https:\/\/doi.org\/10.23919\/DATE.2019.8715061","DOI":"10.23919\/DATE.2019.8715061"},{"key":"391_CR11","doi-asserted-by":"publisher","unstructured":"Ciesielski MJ, Su T, Yasin A, Yu C (2019) Understanding algebraic rewriting for arithmetic circuit verification: a bit-flow model. IEEE TCAD, p\u00a01. https:\/\/doi.org\/10.1109\/TCAD.2019.2912944","DOI":"10.1109\/TCAD.2019.2912944"},{"key":"391_CR12","doi-asserted-by":"publisher","unstructured":"Clegg M, Edmonds J, Impagliazzo R (1996) Using the Groebner basis algorithm to find proofs of unsatisfiability. In: STOC. ACM, pp 174\u2013183. https:\/\/doi.org\/10.1145\/237814.237860","DOI":"10.1145\/237814.237860"},{"key":"391_CR13","doi-asserted-by":"crossref","unstructured":"Cox D, Little J, O\u2019Shea D (1997) Ideals, varieties, and algorithms. Springer-Verlag, New York","DOI":"10.1007\/978-1-4757-2693-0"},{"key":"391_CR14","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe L, Heule MJH, Hunt Jr, WA, Kaufmann M, Schneider-Kamp P (2017) Efficient certified RAT verification. In: de\u00a0Moura L (ed) CADE 26. LNCS, vol 10395. Springer, pp 220\u2013236. https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"issue":"10","key":"391_CR15","doi-asserted-by":"publisher","first-page":"1249","DOI":"10.1090\/noti1173","volume":"61","author":"AJ Dur\u00e1n","year":"2014","unstructured":"Dur\u00e1n AJ, P\u00e9rez M, Varona JL (2014) The misfortunes of a trio of mathematicians using computer algebra systems. can we trust in them? Notices Am. Math. Soc. 61(10):1249\u20131252","journal-title":"Notices Am. Math. Soc."},{"key":"391_CR16","unstructured":"Fleury M, Kaufmann D (2021) Isabelle PAC formalization. http:\/\/people.mpi-inf.mpg.de\/~mfleury\/IsaFoL\/current\/PAC_Checker2\/PAC_Checker\/index.html, theory files at https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/PAC_Checker2\/. Accessed 5 Feb 2021"},{"key":"391_CR17","unstructured":"Fleury M, Kaufmann D (2020) Practical algebraic calculus checker. Arch. Formal Proofs. https:\/\/www.isa-afp.org\/entries\/PAC_Checker.html"},{"key":"391_CR18","doi-asserted-by":"publisher","unstructured":"Haftmann F, Nipkow T (2010) Code generation via higher-order rewrite systems. In: Blume M, Kobayashi N, Vidal G (eds) FLOPS 2010. LNCS, vol\u00a06009. Springer, pp 103\u2013117. https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"391_CR19","unstructured":"Heule MJH (2018) Computing small unit-distance graphs with chromatic number 5. CoRR abs\/1805.12181"},{"key":"391_CR20","doi-asserted-by":"publisher","unstructured":"Heule MJH, Biere A (2015) Proofs for satisfiability problems. In: All about proofs, proofs for all, vol\u00a055, pp 1\u201322. https:\/\/doi.org\/10.1017\/S1471068415000125","DOI":"10.1017\/S1471068415000125"},{"key":"391_CR21","doi-asserted-by":"publisher","unstructured":"Heule MJH, Hunt Jr, WA, Kaufmann M, Wetzler N (2017) Efficient, verified checking of propositional proofs. In: ITP. LNCS, vol 10499. Springer, pp 269\u2013284. https:\/\/doi.org\/10.1007\/978-3-319-66107-0_18","DOI":"10.1007\/978-3-319-66107-0_18"},{"key":"391_CR22","doi-asserted-by":"crossref","unstructured":"Heule MJH, Hunt Jr, WA, Wetzler N (2013) Trimming while checking clausal proofs. In: FMCAD 2013. IEEE, pp 181\u2013188. http:\/\/ieeexplore.ieee.org\/document\/6679408\/","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"391_CR23","doi-asserted-by":"publisher","unstructured":"Heule MJH, Kauers M, Seidl M (2019) Local search for fast matrix multiplication. In: SAT 2019. LNCS, vol 11628. Springer, pp. 155\u2013163. https:\/\/doi.org\/10.1007\/978-3-030-24258-9_10","DOI":"10.1007\/978-3-030-24258-9_10"},{"key":"391_CR24","doi-asserted-by":"publisher","first-page":"899","DOI":"10.1016\/j.jsc.2020.10.003","volume":"104","author":"MJH Heule","year":"2021","unstructured":"Heule MJH, Kauers M, Seidl M (2021) New ways to multiply $$3\\times 3$$-matrices. J Symb Comput 104:899\u2013916","journal-title":"J Symb Comput"},{"issue":"12","key":"391_CR25","doi-asserted-by":"publisher","first-page":"3500","DOI":"10.1093\/ietfec\/e89-a.12.3500","volume":"89\u2013A","author":"N Homma","year":"2006","unstructured":"Homma N, Watanabe Y, Aoki T, Higuchi T (2006) Formal design of arithmetic circuits based on arithmetic description language. IEICE Trans 89\u2013A(12):3500\u20133509","journal-title":"IEICE Trans"},{"issue":"2","key":"391_CR26","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s000370050024","volume":"8","author":"R Impagliazzo","year":"1999","unstructured":"Impagliazzo R, Pudl\u00e1k P, Sgall J (1999) Lower bounds for the polynomial calculus and the Gr\u00f6bner basis algorithm. Comput Complex 8(2):127\u2013144","journal-title":"Comput Complex"},{"key":"391_CR27","doi-asserted-by":"publisher","unstructured":"Kapur D (1986) Geometry theorem proving using Hilbert\u2019s Nullstellensatz. In: SYMSAC. ACM, pp 202\u2013208. https:\/\/doi.org\/10.1145\/32439.32479","DOI":"10.1145\/32439.32479"},{"issue":"4","key":"391_CR28","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/S0747-7171(86)80007-4","volume":"2","author":"D Kapur","year":"1986","unstructured":"Kapur D (1986) Using Gr\u00f6bner bases to reason about geometry problems. J Symb Comput 2(4):399\u2013408. https:\/\/doi.org\/10.1016\/S0747-7171(86)80007-4","journal-title":"J Symb Comput"},{"key":"391_CR29","doi-asserted-by":"crossref","unstructured":"Kapur D, Narendran P (1985) An equational approach to theorem proving in first-order predicate calculus. In: IJCAI. Morgan Kaufmann, pp 1146\u20131153","DOI":"10.1145\/1012497.1012521"},{"key":"391_CR30","unstructured":"Kaufmann D (2021) Nullstellensatz-proofs for multiplier verification. http:\/\/fmv.jku.at\/nussproofs. Accessed 5 Feb 2021"},{"key":"391_CR31","unstructured":"Kaufmann D (2020) Formal verification of multiplier circuits using computer algebra. Ph.D. thesis, Informatik, Johannes Kepler University Linz"},{"key":"391_CR32","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A (2020) Nullstellensatz-proofs for multiplier verification. In: CASC. LNCS, vol 12291. Springer, pp 368\u2013389","DOI":"10.1007\/978-3-030-60026-6_21"},{"key":"391_CR33","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A (2021) AMulet 2.0 for verifying multiplier circuits. In: TACAS (2). Lecture Notes in Computer Science, vol 12652. Springer, pp 357\u2013364","DOI":"10.1007\/978-3-030-72013-1_19"},{"key":"391_CR34","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A, Kauers M (2019) Verifying large multipliers by combining SAT and computer algebra. In: FMCAD 2019. IEEE, pp 28\u201336","DOI":"10.23919\/FMCAD.2019.8894250"},{"key":"391_CR35","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A, Kauers M (2020) From DRUP to PAC and back. In: DATE 2020. IEEE, pp 654\u2013657. http:\/\/fmv.jku.at\/drup2pac\/","DOI":"10.23919\/DATE48585.2020.9116276"},{"key":"391_CR36","doi-asserted-by":"crossref","unstructured":"Kaufmann D, Biere A, Kauers M (2020) SAT, computer algebra, multipliers. In: Vampire 2018 and Vampire 2019. EPiC Series in Computing, vol\u00a071. EasyChair, pp 1\u201318","DOI":"10.29007\/j8cm"},{"key":"391_CR37","unstructured":"Kaufmann D, Fleury M (2021) The LPAC checkers Pacheck 2.0 and past\u00e8que 2.0. http:\/\/fmv.jku.at\/lpac. Accessed 5 Feb 2021"},{"key":"391_CR38","unstructured":"Kaufmann D, Fleury M (2021) The PAC checkers Pacheck and Past\u00e8que. http:\/\/fmv.jku.at\/pacheck_pasteque. Accessed 5 Feb 2021"},{"key":"391_CR39","unstructured":"Kaufmann D, Fleury M, Biere A (2020) Pacheck and Past\u00e8que, Checking Practical Algebraic Calculus Proofs. In: FMCAD 2020. FMCAD, vol\u00a01. TU Vienna Academic Press, pp. 264\u2013269. http:\/\/fmv.jku.at\/pacheck_pasteque\/"},{"key":"391_CR40","doi-asserted-by":"publisher","unstructured":"Lammich P (2015) Refinement to imperative\/HOL. In: Urban C, Zhang X (eds) ITP 2015. LNCS, vol\u00a09236. Springer, pp. 253\u2013269. https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17","DOI":"10.1007\/978-3-319-22102-1_17"},{"key":"391_CR41","doi-asserted-by":"publisher","unstructured":"Lammich P (2016) Refinement based verification of imperative data structures. In: Avigad J, Chlipala A (eds) CPP 2016. ACM Press. pp 27\u201336. https:\/\/doi.org\/10.1145\/2854065.2854067","DOI":"10.1145\/2854065.2854067"},{"key":"391_CR42","doi-asserted-by":"publisher","unstructured":"Lammich P (2017) The GRAT tool chain\u2014efficient (UN)SAT certificate checking with formal correctness guarantees. In: SAT. LNCS, vol 10491. Springer, pp 457\u2013463. https:\/\/doi.org\/10.1007\/978-3-319-66263-3_29","DOI":"10.1007\/978-3-319-66263-3_29"},{"key":"391_CR43","doi-asserted-by":"publisher","unstructured":"Lammich P (2019) Generating verified LLVM from Isabelle\/HOL. In: Tolmach A, Harrison J, O\u2019Leary J (eds) ITP 2019. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.22","DOI":"10.4230\/LIPIcs.ITP.2019.22"},{"issue":"9","key":"391_CR44","first-page":"1409","volume":"32","author":"J Lv","year":"2013","unstructured":"Lv J, Kalla P, Enescu F (2013) Efficient Gr\u00f6bner basis reductions for formal verification of Galois field arithmetic circuits. IEEE TCAD 32(9):1409\u20131420","journal-title":"IEEE TCAD"},{"key":"391_CR45","doi-asserted-by":"publisher","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2018) PolyCleaner: clean your polynomials before backward rewriting to verify million-gate multipliers. In: Bahar I (ed) ICCAD. ACM, p\u00a0129. https:\/\/doi.org\/10.1145\/3240765.3240837","DOI":"10.1145\/3240765.3240837"},{"key":"391_CR46","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2019) RevSCA: using reverse engineering to bring light into backward rewriting for big and dirty multipliers. In: DAC. ACM, pp 185:1\u2013185:6","DOI":"10.1145\/3316781.3317898"},{"key":"391_CR47","doi-asserted-by":"crossref","unstructured":"Mahzoon A, Gro\u00dfe D, Scholl C, Drechsler R (2020) Towards formal verification of optimized and industrial multipliers. In: DATE 2020. IEEE, pp 544\u2013549","DOI":"10.23919\/DATE48585.2020.9116485"},{"key":"391_CR48","unstructured":"Mahzoon A, Gro\u00dfe D, Drechsler R (2019) Multiplier generator GenMul. http:\/\/www.sca-verification.org\/. Accessed 5 Feb 2021"},{"key":"391_CR49","first-page":"18:1","volume":"137","author":"O Meir","year":"2019","unstructured":"Meir O, Nordstr\u00f6m J, Robere R, de Rezende SF (2019) Nullstellensatz size-degree trade-offs from reversible pebbling. ECCC 137:18:1-18:16","journal-title":"ECCC"},{"key":"391_CR50","unstructured":"Miksa M, Nordstr\u00f6m J (2015) A generalized method for proving polynomial calculus degree lower bounds. In: Conference on computational complexity, CCC 2015. LIPIcs, vol\u00a033. Schloss Dagstuhl, pp 467\u2013487"},{"key":"391_CR51","doi-asserted-by":"crossref","unstructured":"Niemetz A, Preiner M, Wolf C, Biere A (2018) Btor2 , BtorMC and Boolector 3.0. In: CAV. LNCS, vol 10981. Springer, pp 587\u2013595","DOI":"10.1007\/978-3-319-96145-3_32"},{"key":"391_CR52","doi-asserted-by":"publisher","unstructured":"Nipkow T, Paulson LC, Wenzel M (2002) Isabelle\/HOL: a proof assistant for higher-order logic, LNCS, vol\u00a02283. Springer. https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"391_CR53","doi-asserted-by":"publisher","unstructured":"Rebola-Pardo A, Altmanninger J (2020) Frying the egg, roasting the chicken: unit deletions in DRAT proofs. In: Blanchette J, Hritcu C (eds) CPP. ACM. https:\/\/doi.org\/10.1145\/3372885","DOI":"10.1145\/3372885"},{"key":"391_CR54","unstructured":"Ritirc D, Biere A, Kauers M (2018) A practical polynomial calculus for arithmetic circuit verification. In: Bigatti A, Brain M (eds) SC2\u201918. CEUR-WS, pp 61\u201376"},{"key":"391_CR55","doi-asserted-by":"crossref","unstructured":"Roche DS (2018) What can (and can\u2019t) we do with sparse polynomials? In: ISSAC. ACM, pp 25\u201330","DOI":"10.1145\/3208976.3209027"},{"key":"391_CR56","doi-asserted-by":"publisher","unstructured":"Soos M, Meel KS (2019) BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In: AAAI 2019. AAAI Press, pp 1592\u20131599. https:\/\/doi.org\/10.1609\/aaai.v33i01.33011592","DOI":"10.1609\/aaai.v33i01.33011592"},{"key":"391_CR57","doi-asserted-by":"crossref","unstructured":"Van\u00a0Gelder A (2008) Verifying RUP proofs of propositional unsatisfiability. In: ISAIM","DOI":"10.1007\/978-3-540-72788-0_31"},{"issue":"4","key":"391_CR58","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10472-012-9322-x","volume":"65","author":"A Van Gelder","year":"2012","unstructured":"Van Gelder A (2012) Producing and verifying extremely large propositional refutations\u2014have your cake and eat it too. Ann Math Artif Intell 65(4):329\u2013372. https:\/\/doi.org\/10.1007\/s10472-012-9322-x","journal-title":"Ann Math Artif Intell"},{"key":"391_CR59","doi-asserted-by":"publisher","unstructured":"Weeks S (2006) Whole-program compilation in MLton. In: Proceedings of the ACM Workshop on ML, 2006, Portland, Oregon, USA, September 16, 2006. ACM Press, p\u00a01. https:\/\/doi.org\/10.1145\/1159876.1159877","DOI":"10.1145\/1159876.1159877"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00391-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-022-00391-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-022-00391-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:22Z","timestamp":1735409002000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-022-00391-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,11]]},"references-count":59,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["391"],"URL":"https:\/\/doi.org\/10.1007\/s10703-022-00391-x","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,11]]},"assertion":[{"value":"1 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 March 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 April 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}