{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T04:02:13Z","timestamp":1750737733855,"version":"3.41.0"},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"unspecified","delay-in-days":43,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2025,5]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents a novel simplification calculus for propositional logic derived from Peirce\u2019s existential graphs\u2019 rules of inference and implication graphs. Our rules can be applied to propositional logic formulae in nested form, are equivalence-preserving, guarantee a monotonically decreasing number of variables, clauses and literals, and maximise the preservation of structural problem information. Our techniques can also be seen as higher-level SAT preprocessing, and we show how one of our rules (TWSR) generalises and streamlines most of the known equivalence-preserving SAT preprocessing methods. In addition, we propose a simplification procedure based on the systematic application of two of our rules (EPR and TWSR) which is solver-agnostic and can be used to simplify large Boolean satisfiability problems and propositional formulae in arbitrary form, and we provide a formal analysis of its algorithmic complexity in terms of space and time. Finally, we show how our rules can be further extended with a novel n-ary implication graph to capture all known equivalence-preserving preprocessing procedures.<\/jats:p>","DOI":"10.1017\/s1471068424000140","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T12:21:43Z","timestamp":1749817303000},"page":"374-393","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["A Novel Framework for Systematic Propositional Formula Simplification Based on Existential Graphs"],"prefix":"10.1017","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-6608-4051","authenticated-orcid":false,"given":"JORDINA","family":"FRANC\u00c8S DE MAS","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JULIANA","family":"BOWLES","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"S1471068424000140_ref1","first-page":"1","volume-title":"25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022","volume":"236","author":"Anders","year":"2022"},{"key":"S1471068424000140_ref22","first-page":"46","volume-title":"Vampire@IJCAR 2016. Proceedings of the 3rd Vampire Workshop","volume":"44","author":"Reger","year":"2016"},{"key":"S1471068424000140_ref15","first-page":"355","volume-title":"Automated Reasoning - 6th International Joint Conference, IJCAR 2012","volume":"7364","author":"J\u00e4rvisalo","year":"2012"},{"key":"S1471068424000140_ref7","first-page":"24","volume-title":"Computer Aided Verification, 22nd International Conference, CAV 2010","volume":"6174","author":"Brayton","year":"2010"},{"unstructured":"Zeman, J. J. 1964. The graphical logic of C. S. Peirce. PhD thesis, The University of Chicago.","key":"S1471068424000140_ref29"},{"key":"S1471068424000140_ref3","first-page":"613","volume-title":"Proceedings of the 18th National Conference on AI and 14th Conference on Innovative Applications of AI","author":"Bacchus","year":"2002"},{"key":"S1471068424000140_ref17","first-page":"291","volume-title":"Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on on Innovative Applications of Artificial Intelligence","author":"Li","year":"2000"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref18","DOI":"10.1016\/j.artint.2019.103197"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref2","DOI":"10.1016\/0020-0190(79)90002-4"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref6","DOI":"10.3233\/FAIA336"},{"key":"S1471068424000140_ref10","first-page":"136","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019","volume":"11628","author":"Fazekas","year":"2019"},{"key":"S1471068424000140_ref5","first-page":"51","volume-title":"Proc. of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions 2020","author":"Biere","year":"2020"},{"unstructured":"Dau, F. 2008. Mathematical Logic with Diagrams \u2013 Based on the Existential Graphs of Peirce. Habilitation thesis, TU Darmstadt, Germany. Unpublished. http:\/\/dr-dau.net\/Papers\/habil.pdf.","key":"S1471068424000140_ref8"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref27","DOI":"10.1515\/semi.2011.060"},{"key":"S1471068424000140_ref13","first-page":"201","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011","volume":"6695","author":"Heule","year":"2011"},{"key":"S1471068424000140_ref16","first-page":"593","article-title":"The map method for synthesis of combinational logic circuits","volume":"72","author":"Karnaugh","year":"1953","journal-title":"Transactions of the American Institute of Electrical Engineers, Part I: Communication and Electronics"},{"key":"S1471068424000140_ref26","first-page":"237","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009","volume":"5584","author":"S\u00f6rensson","year":"2009"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref25","DOI":"10.1023\/A:1008303204427"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref9","DOI":"10.1007\/978-3-540-72788-0_26"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref12","DOI":"10.1090\/dimacs\/026\/27"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref20","DOI":"10.1002\/j.1538-7305.1956.tb03835.x"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref11","DOI":"10.1007\/s10472-005-0433-5"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref4","DOI":"10.1016\/S1571-0653(04)00314-2"},{"doi-asserted-by":"publisher","key":"S1471068424000140_ref23","DOI":"10.1515\/9783110226225"},{"volume-title":"Automation of Reasoning. Symbolic Computation","year":"1983","author":"Tseitin","key":"S1471068424000140_ref28"},{"key":"S1471068424000140_ref19","first-page":"703","volume-title":"Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017","author":"Luo","year":"2017"},{"key":"S1471068424000140_ref14","first-page":"357","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17","volume":"6397","author":"Heule","year":"2010"},{"unstructured":"Peirce, C. 1909. Existential graphs: manuscript 514, with commentary by JF Sowa. Self-published by JF Sowa. [online] URL: http:\/\/www.jfsowa.com\/peirce\/ms514.htm.","key":"S1471068424000140_ref21"},{"unstructured":"Rudell, R. L. 1989. Logic synthesis for VLSI design. Ph.D. thesis, University of California, Berkeley.","key":"S1471068424000140_ref24"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068424000140","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,23]],"date-time":"2025-06-23T10:40:52Z","timestamp":1750675252000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068424000140\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,5]]}},"alternative-id":["S1471068424000140"],"URL":"https:\/\/doi.org\/10.1017\/s1471068424000140","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2025,5]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}