{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T00:23:22Z","timestamp":1742948602261,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031107689"},{"type":"electronic","value":"9783031107696"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe a system that detects an invariance in a logical formula expressing a math problem and simplifies it by eliminating variables utilizing the invariance. Pre-defined function and predicate symbols in the problem representation language are associated with algebraically indexed types, which signify their invariance property. A Hindley-Milner style type reconstruction algorithm is derived for detecting the invariance of a problem. In the experiment, the invariance-based formula simplification significantly enhanced the performance of a problem solver based on quantifier-elimination for real-closed fields, especially on the problems taken from the International Mathematical Olympiads.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_24","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"388-406","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formula Simplification via\u00a0Invariance Detection by Algebraically Indexed Types"],"prefix":"10.1007","author":[{"given":"Takuya","family":"Matsuzaki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomohiro","family":"Fujita","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"24_CR1","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for boolean satisfiability. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence, IJCAI 2003, pp. 271\u2013276 (2003)"},{"issue":"1","key":"24_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/S0304-3975(96)80704-3","volume":"170","author":"NH Arai","year":"1996","unstructured":"Arai, N.H.: Tractability of cut-free Gentzen type propositional calculus with permutation inference. Theoret. Comput. Sci. 170(1), 129\u2013144 (1996)","journal-title":"Theoret. Comput. Sci."},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/10722086_3","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"NH Arai","year":"2000","unstructured":"Arai, N.H., Urquhart, A.: Local symmetries in propositional logic. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 40\u201351. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722086_3"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Atkey, R., Johann, P., Kennedy, A.: Abstraction and invariance for algebraically indexed types. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 87\u2013100 (2013)","DOI":"10.1145\/2480359.2429082"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, pp. 54\u201360 (2007)","DOI":"10.1145\/1277548.1277557"},{"key":"24_CR6","unstructured":"Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning, KR 1996, pp. 148\u2013159 (1996)"},{"issue":"3","key":"24_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/s11786-017-0316-2","volume":"11","author":"JH Davenport","year":"2017","unstructured":"Davenport, J.H.: What does \u201cwithout loss of generality\u2019\u2019 mean, and how do we detect it. Math. Comput. Sci. 11(3), 297\u2013303 (2017)","journal-title":"Math. Comput. Sci."},{"key":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-03359-9_3","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 43\u201359. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_3"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Iwane, H., Anai, H.: Formula simplification for real quantifier elimination using geometric invariance. In: Proceedings of the 2017 ACM on International Symposium on Symbolic and Algebraic Computation, ISSAC 2017, pp. 213\u2013220 (2017)","DOI":"10.1145\/3087604.3087627"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-642-17685-2_8","volume-title":"Central European Functional Programming School","author":"A Kennedy","year":"2010","unstructured":"Kennedy, A.: Types for units-of-measure: theory and practice. In: Horv\u00e1th, Z., Plasmeijer, R., Zs\u00f3k, V. (eds.) CEFP 2009. LNCS, vol. 6299, pp. 268\u2013305. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17685-2_8"},{"issue":"3","key":"24_CR12","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/BF00265682","volume":"22","author":"B Krishnamurthy","year":"1985","unstructured":"Krishnamurthy, B.: Short proofs for tricky formulas. Acta Inform. 22(3), 253\u2013275 (1985)","journal-title":"Acta Inform."},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Matsuzaki, T., Ito, T., Iwane, H., Anai, H., Arai, N.H.: Semantic parsing of pre-university math problems. In: Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2017, pp. 2131\u20132141 (2017)","DOI":"10.18653\/v1\/P17-1195"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Matsuzaki, T., Iwane, H., Anai, H., Arai, N.H.: The most uncreative examinee: a first step toward wide coverage natural language math problem solving. In: Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2014, pp. 1098\u20131104 (2014)","DOI":"10.1609\/aaai.v28i1.8869"},{"issue":"3","key":"24_CR15","doi-asserted-by":"publisher","first-page":"251","DOI":"10.3233\/AIC-180762","volume":"31","author":"T Matsuzaki","year":"2018","unstructured":"Matsuzaki, T., et al.: Can an A.I. win a medal in the mathematical olympiad? - Benchmarking mechanized mathematics on pre-university problems. AI Communications 31(3), 251\u2013266 (2018)","journal-title":"AI Communications"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-319-40229-1_15","volume-title":"Automated Reasoning","author":"T Matsuzaki","year":"2016","unstructured":"Matsuzaki, T., et al.: Race against the teens \u2013 benchmarking mechanized math on pre-university problems. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 213\u2013227. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_15"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-89960-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Metin","year":"2018","unstructured":"Metin, H., Baarir, S., Colange, M., Kordon, F.: CDCLSym: introducing effective symmetry breaking in SAT solving. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 99\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_6"},{"key":"24_CR18","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, pp. 513\u2013523 (1983)"},{"issue":"4","key":"24_CR19","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/s10601-008-9060-1","volume":"14","author":"A Sabharwal","year":"2009","unstructured":"Sabharwal, A.: SymChaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints 14(4), 478\u2013505 (2009)","journal-title":"Constraints"},{"issue":"2","key":"24_CR20","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/S0166-218X(02)00411-0","volume":"130","author":"S Szeider","year":"2003","unstructured":"Szeider, S.: Homomorphisms of conjunctive normal forms. Discrete Appl. Math. 130(2), 351\u2013365 (2003)","journal-title":"Discrete Appl. Math."},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA 1989, pp. 347\u2013359 (1989)","DOI":"10.1145\/99370.99404"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:14:26Z","timestamp":1659316466000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}