{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T22:57:48Z","timestamp":1773442668790,"version":"3.50.1"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031107689","type":"print"},{"value":"9783031107696","type":"electronic"}],"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 , an automated theorem prover for first-order logic that relies on a concurrent search procedure to find tableau proofs, with concurrent processes corresponding to individual branches of the tableau. Since branch closure may require instantiating free variables shared across branches, processes communicate via channels to exchange information about substitutions used for closure. We present the proof search procedure and its implementation, as well as experimental results obtained on problems from the TPTP library.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_22","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"359-368","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Go\u00e9land: A Concurrent Tableau-Based Theorem Prover (System Description)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6665-8089","authenticated-orcid":false,"given":"Julie","family":"Cailler","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1719-2654","authenticated-orcid":false,"given":"Johann","family":"Rosain","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4779-1359","authenticated-orcid":false,"given":"David","family":"Delahaye","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4751-380X","authenticated-orcid":false,"given":"Simon","family":"Robillard","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8749-4562","authenticated-orcid":false,"given":"Hinde Lilia","family":"Bouziane","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-45422-5_29","volume-title":"KI 2001: Advances in Artificial Intelligence","author":"C Benzm\u00fcller","year":"2001","unstructured":"Benzm\u00fcller, C., Kerber, M., Jamnik, M., Sorge, V.: Experiments with an agent-oriented reasoning system. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol. 2174, pp. 409\u2013424. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45422-5_29"},{"key":"22_CR2","unstructured":"Beth, E.W.: Formal Methods: An Introduction to Symbolic Logic and to the Study of Effective Operations in Arithmetic and Logic, Synthese Library, vol. 4. D. Reidel Pub. Co. (1962)"},{"issue":"1","key":"22_CR3","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1023\/A:1018932114059","volume":"29","author":"MP Bonacina","year":"2000","unstructured":"Bonacina, M.P.: A taxonomy of parallel strategies for deduction. Ann. Math. Artif. Intell. 29(1), 223\u2013257 (2000)","journal-title":"Ann. Math. Artif. Intell."},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-319-63516-3_6","volume-title":"Handbook of Parallel Constraint Reasoning","author":"MP Bonacina","year":"2018","unstructured":"Bonacina, M.P.: Parallel theorem proving. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 179\u2013235. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_6"},{"issue":"6","key":"22_CR5","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/s10817-019-09533-z","volume":"64","author":"G Burel","year":"2019","unstructured":"Burel, G., Bury, G., Cauderlier, R., Delahaye, D., Halmagrand, P., Hermant, O.: First-order automated reasoning with theories: when deduction modulo theory meets practice. J. Autom. Reason. 64(6), 1001\u20131050 (2019). https:\/\/doi.org\/10.1007\/s10817-019-09533-z","journal-title":"J. Autom. Reason."},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-319-91271-4_32","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"G Bury","year":"2018","unstructured":"Bury, G., Cruanes, S., Delahaye, D., Euvrard, P.-L.: An automation-friendly set theory for the B method. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 409\u2013414. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_32"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bury, G., Delahaye, D., Doligez, D., Halmagrand, P., Hermant, O.: Automated deduction in the B set theory using typed proof search and deduction modulo. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence and Reasoning (LPAR). EPiC Series in Computing, vol. 35, pp. 42\u201358. EasyChair (2015)","DOI":"10.29007\/14v7"},{"issue":"2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1023\/A:1005879229581","volume":"18","author":"J Denzinger","year":"1997","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT - a distributed and learning equational prover. J. Autom. Reason. 18(2), 189\u2013198 (1997)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"22_CR9","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reason. (JAR) 31(1), 33\u201372 (2003)","journal-title":"J. Autom. Reason. (JAR)"},{"key":"22_CR10","first-page":"80011","volume":"3","author":"M Fisher","year":"1997","unstructured":"Fisher, M.: An open approach to concurrent theorem proving. Parallel Process. Artif. Intell. 3, 80011 (1997)","journal-title":"Parallel Process. Artif. Intell."},{"key":"22_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1990","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, Heidelberg (1990)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/BFb0054245","volume-title":"Automated Deduction \u2014 CADE-15","author":"M Fuchs","year":"1998","unstructured":"Fuchs, M., Wolf, A.: System description: cooperation in model elimination: CPTHEO. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 42\u201346. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054245"},{"key":"22_CR13","first-page":"7","volume":"8","author":"J Hintikka","year":"1955","unstructured":"Hintikka, J.: Two papers on symbolic logic: form and content in quantification theory and reductions in the theory of types. Societas Philosophica, Acta philosophica Fennica 8, 7\u201355 (1955)","journal-title":"Societas Philosophica, Acta philosophica Fennica"},{"issue":"8","key":"22_CR14","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BFb0055140","volume-title":"Theorem Proving in Higher Order Logics","author":"K Konrad","year":"1998","unstructured":"Konrad, K.: Hot: a concurrent automated theorem prover based on higher-order tableaux. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 245\u2013261. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055140"},{"issue":"1","key":"22_CR16","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"RE Korf","year":"1985","unstructured":"Korf, R.E.: Depth-first iterative-deepening: an optimal admissible tree search. Artif. Intell. 27(1), 97\u2013109 (1985)","journal-title":"Artif. Intell."},{"key":"22_CR17","doi-asserted-by":"publisher","unstructured":"Letz, R.: First-order tableau methods. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 125\u2013196. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/978-94-017-1754-0_3. ISBN 978-94-017-1754-0","DOI":"10.1007\/978-94-017-1754-0_3"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-52885-7_78","volume-title":"10th International Conference on Automated Deduction","author":"J Schumann","year":"1990","unstructured":"Schumann, J., Letz, R.: Partheo: a high-performance parallel theorem prover. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 40\u201356. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_78"},{"issue":"4","key":"22_CR19","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. (JAR) 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason. (JAR)"},{"key":"22_CR20","unstructured":"Tsoukalos, M.: Mastering Go: Create Golang Production Applications Using Network Libraries, Concurrency, Machine Learning, and Advanced Data Structures, pp. 439\u2013463. Packt Publishing Ltd. (2019)"},{"issue":"3","key":"22_CR21","doi-asserted-by":"publisher","first-page":"554","DOI":"10.1016\/j.eswa.2005.04.013","volume":"29","author":"CH Wu","year":"2005","unstructured":"Wu, C.H.: A multi-agent framework for distributed theorem proving. Expert Syst. Appl. 29(3), 554\u2013565 (2005)","journal-title":"Expert Syst. Appl."}],"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_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T09:31:08Z","timestamp":1727688668000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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)"}}]}}