{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T12:03:14Z","timestamp":1790596994731,"version":"4.1.0"},"reference-count":64,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,9,1]],"date-time":"2026-09-01T00:00:00Z","timestamp":1788220800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,8,12]],"date-time":"2026-08-12T00:00:00Z","timestamp":1786492800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003359","name":"Generalitat Valenciana","doi-asserted-by":"publisher","award":["CIPROM\/2022\/6"],"award-info":[{"award-number":["CIPROM\/2022\/6"]}],"id":[{"id":"10.13039\/501100003359","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,9]]},"DOI":"10.1016\/j.jlamp.2026.101155","type":"journal-article","created":{"date-parts":[[2026,8,7]],"date-time":"2026-08-07T06:44:23Z","timestamp":1786085063000},"page":"101155","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["NuITP: Accelerating the inductive verification of equational programs through symbolic simplification"],"prefix":"10.1016","volume":"151","author":[{"given":"Francisco","family":"Dur\u00e1n","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julia","family":"Sapi\u00f1a","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2026.101155_bib0001","article-title":"All About Maude: A High-Performance Logical Framework","volume":"Vol. 4350","author":"Clavel","year":"2007"},{"key":"10.1016\/j.jlamp.2026.101155_bib0002","article-title":"CafeOBJ Report","volume":"Vol. 6","author":"Diaconescu","year":"1998"},{"key":"10.1016\/j.jlamp.2026.101155_bib0003","series-title":"Software Engineering with OBJ: Algebraic Specification in Action, Advances in Formal Methods","first-page":"3","article-title":"Introducing OBJ","author":"Goguen","year":"2000"},{"key":"10.1016\/j.jlamp.2026.101155_bib0004","article-title":"Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification","volume":"144","author":"Meseguer","year":"2025","journal-title":"J. Log. Algebr. Methods Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0005","series-title":"Proceedings of the 26th International Symposium on Principles and Practice of Declarative Programming (PPDP 2024)","first-page":"6:1","article-title":"NuITP: an inductive theorem prover for equational program verification","author":"Dur\u00e1n","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101155_sbref0006","series-title":"Technical Report","article-title":"Proofs for the Proof Obligations of the Paper \u201cNuITP: Accelerating the Inductive Verification of Equational Programs through Symbolic Simplification\u201d","author":"Dur\u00e1n","year":"2026"},{"key":"10.1016\/j.jlamp.2026.101155_bib0007","series-title":"Proceedings of the 7th ACM-SIGACT Symposium on Principles of Programming Languages (POPL 1980)","first-page":"154","article-title":"On proving inductive properties of abstract data types","author":"Musser","year":"1980"},{"key":"10.1016\/j.jlamp.2026.101155_bib0008","series-title":"Proceedings of the 5th International Conference on Automated Deduction (CADE 1980)","first-page":"356","article-title":"How to prove algebraic inductive hypotheses without induction: with applications to the correctness of data type implementation","volume":"Vol. 87","author":"Goguen","year":"1980"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101155_bib0009","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","article-title":"Proofs by induction in equational theories with constructors","volume":"25","author":"Huet","year":"1982","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"10.1016\/j.jlamp.2026.101155_bib0010","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","article-title":"Proof by consistency","volume":"31","author":"Kapur","year":"1987","journal-title":"Artif. Intell."},{"key":"10.1016\/j.jlamp.2026.101155_bib0011","series-title":"Proceedings of the 3rd Annual Symposium on Logic in Computer Science (LICS 1988)","first-page":"228","article-title":"Proof by consistency in equational theories","author":"Bachmair","year":"1988"},{"issue":"2","key":"10.1016\/j.jlamp.2026.101155_bib0012","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881856","article-title":"Implicit induction in conditional theories","volume":"14","author":"Bouhoula","year":"1995","journal-title":"J. Autom. Reason."},{"issue":"1\u20132","key":"10.1016\/j.jlamp.2026.101155_bib0013","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1006\/inco.2000.2875","article-title":"Induction=I-Axiomatization+first-order consistency","volume":"159","author":"Comon","year":"2000","journal-title":"Inf. Comput."},{"key":"10.1016\/j.jlamp.2026.101155_bib0014","series-title":"Programming Logics - Essays in Memory of Harald Ganzinger","first-page":"216","article-title":"Narrowing based inductive proof search","volume":"Vol. 7797","author":"Kirchner","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101155_bib0015","series-title":"Proc. RTA-89","first-page":"559","article-title":"An overview of rewrite rule laboratory (RRL)","volume":"Vol. 355","author":"Kapur","year":"1989"},{"key":"10.1016\/j.jlamp.2026.101155_bib0016","series-title":"Proceedings of the 2nd International Workshop on Algebraic and Logic Programming (ALP 1990)","first-page":"1","article-title":"Proving and rewriting","volume":"Vol. 463","author":"Goguen","year":"1990"},{"key":"10.1016\/j.jlamp.2026.101155_bib0017","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2704-5","article-title":"Larch: Languages and Tools for Formal Specification","author":"Guttag","year":"1993"},{"key":"10.1016\/j.jlamp.2026.101155_bib0018","series-title":"CAFE: An Industrial-Strength Algebraic Formal Method","first-page":"1","article-title":"Building equational proving tools by reflection in rewriting logic","author":"Clavel","year":"2000"},{"key":"10.1016\/j.jlamp.2026.101155_bib0019","series-title":"Specification, Algebra, and Software - Essays Dedicated to Kokichi Futatsugi","first-page":"578","article-title":"On automation of OTS\/CafeOBJ method","volume":"Vol. 8373","author":"G\u00e2in\u00e2","year":"2014"},{"key":"10.1016\/j.jlamp.2026.101155_bib0020","series-title":"The ITP Tool\u2019s Manual","author":"Clavel","year":"2005"},{"key":"10.1016\/j.jlamp.2026.101155_sbref0021","series-title":"Decision Procedures for Equationally Based Reasoning","author":"Hendrix","year":"2008"},{"key":"10.1016\/j.jlamp.2026.101155_bib0022","series-title":"ITP 2010","first-page":"275","article-title":"Coverset induction with partiality and subsorts: a powerlist case study","volume":"Vol. 6172","author":"Hendrix","year":"2010"},{"key":"10.1016\/j.jlamp.2026.101155_bib0023","article-title":"Theorem proving and algebra","author":"Goguen","year":"2021","journal-title":"CoRR"},{"key":"10.1016\/j.jlamp.2026.101155_bib0024","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2022.102893","article-title":"Advances of proof scores in CafeOBJ","volume":"224","author":"Futatsugi","year":"2022","journal-title":"Sci. Comput. Program."},{"issue":"3","key":"10.1016\/j.jlamp.2026.101155_bib0025","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","article-title":"Rewrite-based equational theorem proving with selection and simplification","volume":"4","author":"Bachmair","year":"1994","journal-title":"J. Log. Comput."},{"issue":"2\u20133","key":"10.1016\/j.jlamp.2026.101155_bib0026","first-page":"111","article-title":"E \u2013 a brainiac theorem prover","volume":"15","author":"Schulz","year":"2002","journal-title":"AI Commun."},{"key":"10.1016\/j.jlamp.2026.101155_bib0027","series-title":"Automated Deduction \u2013 CADE-22","first-page":"140","article-title":"SPASS Version 3.5","author":"Weidenbach","year":"2009"},{"key":"10.1016\/j.jlamp.2026.101155_bib0028","series-title":"25th International Conference on Automated Deduction (CADE 2025)","first-page":"378","article-title":"The Lean theorem prover (system description)","volume":"Vol. 9195","author":"de Moura","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101155_bib0029","unstructured":"T.C.D. Team, The Coq Proof Assistant Reference Manual, 2026. Version 9.2.0, https:\/\/rocq-prover.org."},{"key":"10.1016\/j.jlamp.2026.101155_bib0030","article-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","volume":"Vol. 2283","author":"Nipkow","year":"2002"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101155_bib0031","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","article-title":"Extending Sledgehammer with SMT solvers","volume":"51","author":"Blanchette","year":"2013","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.jlamp.2026.101155_bib0032","series-title":"25th International Conference on Computer Aided Verification (CAV 2013)","first-page":"1","article-title":"First-order theorem proving and Vampire","volume":"Vol. 8044","author":"Kov\u00e1cs","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101155_bib0033","series-title":"19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-19)","first-page":"735","article-title":"System description: E 1.8","volume":"8312","author":"Schulz","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101155_bib0034","series-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008)","first-page":"337","article-title":"Z3: an efficient SMT solver","volume":"Vol. 4963","author":"de Moura","year":"2008"},{"key":"10.1016\/j.jlamp.2026.101155_bib0035","series-title":"28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)","first-page":"415","article-title":"cvc5: a versatile and industrial-strength SMT solver","volume":"13243","author":"Barbosa","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101155_bib0036","series-title":"Proceedings of the Workshop on Practical Aspects of Automated Reasoning","article-title":"The Vampire approach to induction (short paper)","volume":"Vol. 3201","author":"Hajd\u00fa","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101155_bib0037","series-title":"16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2015)","first-page":"80","article-title":"Induction for SMT solvers","volume":"Vol. 8931","author":"Reynolds","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101155_bib0038","series-title":"23rd International Conference on Formal Engineering Methods (ICFEM 2022)","first-page":"263","article-title":"Theorem proving for Maude specifications using Lean","volume":"Vol. 13478","author":"Rubio","year":"2022"},{"key":"10.1016\/j.jlamp.2026.101155_bib0039","article-title":"Maude2Lean: theorem proving for Maude specifications using Lean","volume":"142","author":"Rubio","year":"2025","journal-title":"J. Log. Algebraic Methods Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0040","series-title":"13th International Conference on Algebraic Methodology and Software Technology (AMAST 2010)","first-page":"60","article-title":"Integrating Maude into Hets","volume":"Vol. 6486","author":"Codescu","year":"2010"},{"key":"10.1016\/j.jlamp.2026.101155_bib0041","series-title":"7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018)","first-page":"14","article-title":"Total Haskell is reasonable Coq","author":"Spector-Zabusky","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101155_bib0042","series-title":"15th ACM SIGPLAN International Conference on Functional Programming (ICFP 2010)","first-page":"321","article-title":"Program verification through characteristic formulae","author":"Chargu\u00e9raud","year":"2010"},{"key":"10.1016\/j.jlamp.2026.101155_bib0043","series-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann","year":"2000"},{"issue":"11","key":"10.1016\/j.jlamp.2026.101155_bib0044","first-page":"1618","article-title":"Introducing the ITP tool: a tutorial","volume":"12","author":"Clavel","year":"2006","journal-title":"J. Univers. Comput. Sci."},{"key":"10.1016\/j.jlamp.2026.101155_bib0045","series-title":"Decision Procedures for Equationally Based Reasoning","author":"Hendrix","year":"2008"},{"key":"10.1016\/j.jlamp.2026.101155_bib0046","series-title":"A Computational Logic","author":"Boyer","year":"1980"},{"key":"10.1016\/j.jlamp.2026.101155_bib0047","series-title":"9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23\u201326, 1988, Proceedings","first-page":"162","article-title":"A mechanizable induction principle for equational specifications","volume":"310","author":"Zhang","year":"1988"},{"key":"10.1016\/j.jlamp.2026.101155_bib0048","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/j.scico.2014.07.003","article-title":"Order-sorted equality enrichments modulo axioms","volume":"99","author":"Guti\u00e9rrez","year":"2015","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0049","series-title":"Foundations of Security Analysis and Design V, FOSAD 2007\/2008\/2009 Tutorial Lectures","first-page":"1","article-title":"Maude-NPA: cryptographic protocol analysis modulo equational properties","volume":"Vol. 5705","author":"Escobar","year":"2009"},{"key":"10.1016\/j.jlamp.2026.101155_bib0050","series-title":"Proc. CAV 2013","first-page":"696","article-title":"The TAMARIN prover for the symbolic analysis of security protocols","volume":"Vol. 8044","author":"Meier","year":"2013"},{"key":"10.1016\/j.jlamp.2026.101155_bib0051","series-title":"Proc. WRLA 2026","first-page":"96","article-title":"Generating invariants by deductive model checking","author":"Bae","year":"2026"},{"key":"10.1016\/j.jlamp.2026.101155_bib0052","article-title":"DM-Check: verifying invariants of concurrent systems by deductive model checking","volume":"149","author":"Bae","year":"2026","journal-title":"J. Log. Algebr. Methods Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0053","series-title":"Proc. WRLA 2020","first-page":"114","article-title":"Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification","volume":"Vol. 12328","author":"Meseguer","year":"2020"},{"issue":"1","key":"10.1016\/j.jlamp.2026.101155_bib0054","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","article-title":"Conditional rewriting logic as a unified model of concurrency","volume":"96","author":"Meseguer","year":"1992","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"10.1016\/j.jlamp.2026.101155_bib0055","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/j.jlamp.2015.06.001","article-title":"Normal forms and normal theories in conditional rewriting","volume":"85","author":"Lucas","year":"2016","journal-title":"J. Log. Algebr. Meth. Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0056","series-title":"Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005)","first-page":"294","article-title":"The finite variant property: how to get rid of some algebraic properties","volume":"Vol. 3467","author":"Comon-Lundh","year":"2005"},{"issue":"7\u20138","key":"10.1016\/j.jlamp.2026.101155_bib0057","doi-asserted-by":"crossref","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","article-title":"Folding variant narrowing and optimal variant termination","volume":"81","author":"Escobar","year":"2012","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0058","first-page":"81","article-title":"Metalevel algorithms for variant satisfiability","volume":"96","author":"Skeirik","year":"2018","journal-title":"J. Log. Algebr. Methods Program."},{"key":"10.1016\/j.jlamp.2026.101155_sbref0060","series-title":"Technical Report","article-title":"Maude Manual (Version 3.5.1)","author":"Clavel","year":"2025"},{"key":"10.1016\/j.jlamp.2026.101155_bib0060","series-title":"Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2016)","first-page":"493","article-title":"Order-Sorted rewriting and congruence closure","volume":"Vol. 9634","author":"Meseguer","year":"2016"},{"key":"10.1016\/j.jlamp.2026.101155_bib0061","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/j.jlamp.2026.101155_sbref0063","series-title":"Technical Report","article-title":"NuITP User\u2019s Manual","author":"Dur\u00e1n","year":"2025"},{"key":"10.1016\/j.jlamp.2026.101155_bib0063","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.scico.2017.09.001","article-title":"Variant-based satisfiability in initial algebras","volume":"154","author":"Meseguer","year":"2018","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.jlamp.2026.101155_bib0064","unstructured":"S. Eker, A pragmatic approach to implementing associative unification, 2015Unpublished manuscript, SRI International, circa."}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000477?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000477?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,9,28]],"date-time":"2026-09-28T11:43:14Z","timestamp":1790595794000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000477"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9]]},"references-count":64,"alternative-id":["S2352220826000477"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101155","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,9]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"NuITP: Accelerating the inductive verification of equational programs through symbolic simplification","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101155","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Authors. Published by Elsevier Inc.","name":"copyright","label":"Copyright"}],"article-number":"101155"}}