{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T23:35:52Z","timestamp":1783726552628,"version":"3.55.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T00:00:00Z","timestamp":1760572800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T00:00:00Z","timestamp":1760572800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"DOI":"10.1007\/s10817-025-09742-9","type":"journal-article","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:29:42Z","timestamp":1760596182000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Theorem Proving as Constraint Solving for Coherent Logic with Function Symbols"],"prefix":"10.1007","volume":"69","author":[{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,16]]},"reference":[{"key":"9742_CR1","unstructured":"Atocha, A.: Abductive Reasoning, volume 330 of Synthese Library. Kluwer Academic Publishers, Dordrecht (2006)"},{"key":"9742_CR2","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Byli\u0144ski, C., Grabowski, A., Korni\u0142owicz, A., Matuszewski, R., Naumowicz, A., Pak, K., Urban, J.: Mizar: State-of-the-art and beyond. In Intelligent Computer Mathematics \u2013 International Conference, CICM 2015, Washington, DC, USA, July 13\u201317, 2015, Proceedings, pages 261\u2013279, (2015)","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"9742_CR3","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Keller, C., Reynolds, A., Viswanathan, A., Tinelli, C., Barrett, C.W.: An interactive SMT tactic in coq using abductive reasoning. In Ruzica Piskac and Andrei Voronkov, editors, LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Manizales, Colombia, 4-9th June 2023, volume 94 of EPiC Series in Computing, pages 11\u201322. EasyChair, (2023)","DOI":"10.29007\/432m"},{"issue":"1\u20132","key":"9742_CR4","first-page":"21","volume":"3","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput. 3(1\u20132), 21\u201346 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9742_CR5","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Tinelli, C., Barbosa, H., Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y.: Satisfiability modulo theories: A beginner\u2019s tutorial. In Platzer, A., Rozier, K.Y., Pradella, M., Rossi, M., editors, Formal Methods - 26th International Symposium, FM 2024, Milan, Italy, September 9-13, 2024, Proceedings, Part II, volume 14934 of Lecture Notes in Computer Science, pages 571\u2013596. Springer, (2024)","DOI":"10.1007\/978-3-031-71177-0_31"},{"key":"9742_CR6","doi-asserted-by":"crossref","unstructured":"M. Beeson, J. Narboux, and F. Wiedijk. Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence, 85(2-4):213\u2013257, 2019. Publisher: Springer","DOI":"10.1007\/s10472-018-9606-x"},{"key":"9742_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive theorem proving and program development: Coq\u2019Art: the calculus of inductive constructions. Springer, Berlin (2004)"},{"key":"9742_CR8","doi-asserted-by":"crossref","unstructured":"Bezem, M.: On the Undecidability of Coherent Logic. In Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 6\u201313. Springer, (2005)","DOI":"10.1007\/11601548_2"},{"key":"9742_CR9","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1142\/9789812562494_0050","volume":"2","author":"M Bezem","year":"2004","unstructured":"Bezem, M., Coquand, T.: Newman\u2019s lemma - a case study in proof automation and geometric logic. Current trends in Theoretical Computer Science 2, 267\u2013282 (2004)","journal-title":"Current trends in Theoretical Computer Science"},{"key":"9742_CR10","doi-asserted-by":"crossref","unstructured":"Bezem, M., Coquand, T.: Automating Coherent Logic. In Geoff Sutcliffe and Andrei Voronkov, editors, 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning \u2014 LPAR 2005, volume 3835 of Lecture Notes in Computer Science, pages 246\u2013260. Springer-Verlag, (2005)","DOI":"10.1007\/11591191_18"},{"issue":"1","key":"9742_CR11","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/s10817-007-9086-x","volume":"40","author":"M Bezem","year":"2008","unstructured":"Bezem, M., Hendriks, D.: On the mechanization of the proof of hessenberg\u2019s theorem in coherent logic. J. Autom. Reason. 40(1), 61\u201385 (2008)","journal-title":"J. Autom. Reason."},{"key":"9742_CR12","doi-asserted-by":"crossref","unstructured":"Jeremy Bongio, Cyrus Katrak, Hai Lin, Christopher Lynch, and Ralph\u00a0Eric McGregor. Encoding First Order Proofs in SMT. Electron. Notes Theor. Comput. Sci., 198(2):71\u201384, 2008","DOI":"10.1016\/j.entcs.2008.04.081"},{"key":"9742_CR13","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In Tetsuo Ida and Jacques Fleuriot, editors, Post-proceedings of Automated Deduction in Geometry 2012, volume 7993 of LNCS, pages 89\u2013109, Edinburgh, United Kingdom, September 2012. Springer","DOI":"10.1007\/978-3-642-40672-0_7"},{"issue":"1","key":"9742_CR14","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-013-9283-8","volume":"51","author":"CE Brown","year":"2013","unstructured":"Brown, C.E.: Reducing higher-order theorem proving to a sequence of sat problems. J. Autom. Reason. 51(1), 57\u201377 (2013)","journal-title":"J. Autom. Reason."},{"key":"9742_CR15","doi-asserted-by":"crossref","unstructured":"Cailler, J., Rosain, J., Delahaye, D., Robillard, S., Bouziane, H.-L.: Go\u00e9land: A concurrent tableau-based theorem prover (system description). In Jasmin Blanchette, Laura Kov\u00e1cs, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings, volume 13385 of Lecture Notes in Computer Science, pages 359\u2013368. Springer, (2022)","DOI":"10.1007\/978-3-031-10769-6_22"},{"key":"9742_CR16","doi-asserted-by":"crossref","unstructured":"D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.): Handbook of Tableau Methods. Springer, Berlin (1999)","DOI":"10.1007\/978-94-017-1754-0"},{"key":"9742_CR17","doi-asserted-by":"crossref","unstructured":"Denecker, M., Kakas, A.C.: Abduction in Logic Programming. In Kakas, A.C., Sadri, F., editors, Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part I, volume 2407 of Lecture Notes in Computer Science, pages 402\u2013436. Springer, (2002)","DOI":"10.1007\/3-540-45628-7_16"},{"key":"9742_CR18","doi-asserted-by":"crossref","unstructured":"Deshane, T., Hu, W., Jablonski, P., Lin, H., Lynch, C., McGregor, R.E.: Encoding First Order Proofs in SAT. In Pfenning, F., editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages 476\u2013491. Springer, (2007)","DOI":"10.1007\/978-3-540-73595-3_35"},{"key":"9742_CR19","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T.: Explain: a tool for performing abductive inference. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, pp. 684\u2013689. Heidelberg, Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39799-8_46"},{"key":"9742_CR20","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1017\/bsl.2015.7","volume":"21","author":"R Dyckhoff","year":"2015","unstructured":"Dyckhoff, R., Negri, S.: Geometrization of first-order logic. Bull. Symb. Log. 21, 123\u2013163 (2015)","journal-title":"Bull. Symb. Log."},{"key":"9742_CR21","volume-title":"Symbolic Logic: An introduction","author":"F Fitch","year":"1952","unstructured":"Fitch, F.: Symbolic Logic: An introduction. The Ronald Press Company, New York (1952)"},{"key":"9742_CR22","doi-asserted-by":"crossref","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schliessen, I, II. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935. English translation in \u201cThe Collected Papers of Gerhard Gentzen\u201d, North-Holland Publ.Co, 1969","DOI":"10.1007\/BF01201363"},{"key":"9742_CR23","unstructured":"Holen, B., Hovland, D., Giese, M.: Efficient Rule-Matching for Automated Coherent Logic. In NIK-2013 proceedings, (2012)"},{"issue":"3","key":"9742_CR24","first-page":"30","volume":"8","author":"P Jani\u010di\u0107","year":"2012","unstructured":"Jani\u010di\u0107, P.: Ursa: a system for uniform reduction to sat. Logical Methods in Computer Science 8(3), 30 (2012)","journal-title":"Logical Methods in Computer Science"},{"key":"9742_CR25","doi-asserted-by":"crossref","unstructured":"Jani\u010di\u0107, P.: GCLC \u2014 A Tool for Constructive Euclidean Geometry and More Than That. In Iglesias, A., Takayama, N., editors, Mathematical Software - ICMS 2006, volume 4151 of Lecture Notes in Computer Science, pages 58\u201373. Springer, (2006)","DOI":"10.1007\/11832225_6"},{"issue":"1\u20132","key":"9742_CR26","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-009-9135-8","volume":"44","author":"P Jani\u010di\u0107","year":"2010","unstructured":"Jani\u010di\u0107, P.: Geometry constructions language. J. Autom. Reason. 44(1\u20132), 3\u201324 (2010)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9742_CR27","first-page":"723","volume":"9","author":"P Jani\u010di\u0107","year":"1995","unstructured":"Jani\u010di\u0107, P., Kordi\u0107, S.: Euclid \u2013 the geometry theorem prover. FILOMAT 9(3), 723\u2013732 (1995)","journal-title":"FILOMAT"},{"issue":"4","key":"9742_CR28","doi-asserted-by":"publisher","first-page":"689","DOI":"10.1007\/s10817-022-09629-z","volume":"66","author":"P Jani\u010di\u0107","year":"2022","unstructured":"Jani\u010di\u0107, P., Narboux, J.: Theorem proving as constraint solving with coherent logic. J. Autom. Reason. 66(4), 689\u2013746 (2022)","journal-title":"J. Autom. Reason."},{"key":"9742_CR29","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1007\/s10472-023-09857-y","volume":"91","author":"P Jani\u010di\u0107","year":"2023","unstructured":"Jani\u010di\u0107, P., Narboux, J.: Automated generation of illustrated proofs in geometry and beyond. Ann. Math. Artif. Intell. 91, 797\u2013820 (2023)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9742_CR30","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-Order Theorem Proving and Vampire. In Sharygina, N., Veith, H., editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 1\u201335. Springer, (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9742_CR31","volume-title":"Beginning Logic","author":"Edward John Lemmon","year":"1965","unstructured":"Edward John Lemmon: Beginning Logic. Thomas Nelson and Sons Ltd, Nashville (1965)"},{"key":"9742_CR32","volume-title":"Fundamentals of Artificial Intelligence Research","author":"P Marquis","year":"1991","unstructured":"Marquis, P.: Extending abduction from propositional to first-order logic. In: Jorrand, P., Kelemen, J. (eds.) Fundamentals of Artificial Intelligence Research. Springer, Heidelberg (1991)"},{"key":"9742_CR33","unstructured":"McGregor, R.E.: Automated Theorem Proving Using SAT. PhD Thesis, Clarkson University, (2011)"},{"key":"9742_CR34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Springer, Heidelberg (2008)"},{"key":"9742_CR35","unstructured":"Nikoli\u0107, M., Jani\u010di\u0107, P.: CDCL-Based Abstract State Transition System for Coherent Logic. In Jeuring, J., Campbell, J.A., Carette, J., Reis, G.D., Sojka, P., Wenzel, M., Sorge, V., editors, Intelligent Computer Mathematics - 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of Lecture Notes in Computer Science, pages 264\u2013279. Springer, (2012)"},{"key":"9742_CR36","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle HOL: a Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, (2002)","DOI":"10.1007\/3-540-45949-9"},{"issue":"2","key":"9742_CR37","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1093\/logcom\/exu071","volume":"27","author":"H de Nivelle","year":"2017","unstructured":"de Nivelle, H.: Theorem proving for classical logic with partial functions by reduction to kleene logic. J. Log. Comput. 27(2), 509\u2013548 (2017)","journal-title":"J. Log. Comput."},{"key":"9742_CR38","unstructured":"Polonsky, A.: Proofs, Types and Lambda Calculus. PhD thesis, University of Bergen, (2011)"},{"key":"9742_CR39","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Larraz, D., Tinelli, C.: Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I, volume 12166 of Lecture Notes in Computer Science, pages 141\u2013160. Springer, (2020)","DOI":"10.1007\/978-3-030-51074-9_9"},{"key":"9742_CR40","doi-asserted-by":"crossref","unstructured":"Russo, A., Nuseibeh, B.: On The Use Of Logical Abduction In Software Engineering. (2001)","DOI":"10.1142\/9789812389718_0037"},{"key":"9742_CR41","doi-asserted-by":"crossref","unstructured":"Stephan Schulz. Light-weight integration of SAT solving into first-order reasoners\u2013first experiments. Vampire 2017 - Proceedings of the 4th Vampire Workshop, 53:9\u201319, 2017","DOI":"10.29007\/89kc"},{"key":"9742_CR42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-69418-9","volume-title":"Metamathematische Methoden in der Geometrie","author":"W Schwabh\u00e4user","year":"1983","unstructured":"Schwabh\u00e4user, W., Szmielew, W., Tarski, A.: Metamathematische Methoden in der Geometrie. Springer-Verlag, Berlin (1983)"},{"key":"9742_CR43","doi-asserted-by":"crossref","unstructured":"Stojanovi\u0107, S., Narboux, J., Bezem, M., Jani\u010di\u0107, P.: A Vernacular for Coherent Logic. In Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J., editors, Intelligent Computer Mathematics, volume 8543 of Lecture Notes in Computer Science, pages 388\u2013403. Springer International Publishing, (2014)","DOI":"10.1007\/978-3-319-08434-3_28"},{"key":"9742_CR44","doi-asserted-by":"crossref","unstructured":"Stojanovi\u0107, S., Pavlovi\u0107, V., Jani\u010di\u0107, P.: A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs. In Automated Deduction in Geometry, volume 6877 of Lecture Notes in Computer Science, pages 201\u2013220. Springer, (2011)","DOI":"10.1007\/978-3-642-25070-5_12"},{"key":"9742_CR45","doi-asserted-by":"crossref","unstructured":"Gonzalez, S.T., Jani\u010di\u0107, P., Narboux, J.: Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving. In Proceedings of the 14th International Conference on Automated Deduction in Geometry 2023, volume EPTCS 398, pages 21\u201337, Belgrade, Serbia, September (2023)","DOI":"10.4204\/EPTCS.398.6"},{"key":"9742_CR46","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: AVATAR: The Architecture for First-Order Theorem Provers. In Computer Aided Verification, pages 696\u2013710. Springer, Cham, July 2014","DOI":"10.1007\/978-3-319-08867-9_46"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09742-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09742-9","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09742-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:30Z","timestamp":1766134230000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09742-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,16]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9742"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09742-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,16]]},"assertion":[{"value":"23 October 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 October 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"29"}}