{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:18:51Z","timestamp":1758266331002,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,4,1]],"date-time":"2012-04-01T00:00:00Z","timestamp":1333238400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2012,4]]},"abstract":"<jats:p>The implementation of a logic requires, besides the definition of a calculus and a decision procedure, the development of techniques to reduce the search space. In this article we introduce some simplification rules for Intuitionistic propositional logic that try to replace a formula with an equi-satisfiable \u201csimpler\u201d one with the aim to reduce the search space. Our results are proved via semantical techniques based on Kripke models. We also provide an empirical evaluation of their impact on implementations.<\/jats:p>","DOI":"10.1145\/2159531.2159536","type":"journal-article","created":{"date-parts":[[2012,4,24]],"date-time":"2012-04-24T18:41:10Z","timestamp":1335292870000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Simplification Rules for Intuitionistic Propositional Tableaux"],"prefix":"10.1145","volume":"13","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi dell\u2019Insubria"}]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano"}]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano-Bicocca"}]}],"member":"320","published-online":{"date-parts":[[2012,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00044-X"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/7.4.447"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.013"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Chagrov A. and Zakharyaschev M. 1997. Modal Logic. Oxford University Press. Chagrov A. and Zakharyaschev M. 1997. Modal Logic . Oxford University Press.","DOI":"10.1093\/oso\/9780198537793.001.0001"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(84)90014-1"},{"volume-title":"Fcube: An efficient prover for intuitionistic propositional logic. In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning","year":"2010","author":"Ferrari M.","key":"e_1_2_1_7_1"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Hustadt U. and Schmidt R. A . 1998 . Simplification and backjumping in modal tableau. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX\u201998). H. C. M. de Swart Ed . Lecture Notes in Computer Science vol. 1397 187--201. Hustadt U. and Schmidt R. A. 1998. Simplification and backjumping in modal tableau. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX\u201998) . H. C. M. de Swart Ed. Lecture Notes in Computer Science vol. 1397 187--201.","DOI":"10.1007\/3-540-69778-0_22"},{"volume-title":"Mathematical Logic","author":"Kleene S.","key":"e_1_2_1_9_1"},{"volume-title":"Strip: Structural sharing for efficient proofsearch. In Proceedings of the 1st International Joint Conference on Automated Reasoning","year":"2001","author":"Larchey-Wendling D.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/646889.709129"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_12"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9060-z"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"volume-title":"First-Order Logic","author":"Smullyan R.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/646889.709111"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006351428454"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159536","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2159531.2159536","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:59:58Z","timestamp":1750244398000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2159531.2159536"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["10.1145\/2159531.2159536"],"URL":"https:\/\/doi.org\/10.1145\/2159531.2159536","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2012,4]]},"assertion":[{"value":"2010-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2012-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}