{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:57Z","timestamp":1776333417602,"version":"3.51.2"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Superposition is among the most successful calculi for first-order logic. Its extension to higher-order logic introduces new challenges such as infinitely branching inference rules, new possibilities such as reasoning about formulas, and the need to curb the explosion of specific higher-order rules. We describe techniques that address these issues and extensively evaluate their implementation in the Zipperposition theorem prover. Largely thanks to their use, Zipperposition won the higher-order division of the CASC-J10 competition.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_24","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"415-432","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Making Higher-Order Superposition Work"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7049-6847","authenticated-orcid":false,"given":"Petar","family":"Vukmirovi\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7158-3595","authenticated-orcid":false,"given":"Alexander","family":"Bentkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3969-5850","authenticated-orcid":false,"given":"Simon","family":"Cruanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0078-790X","authenticated-orcid":false,"given":"Visa","family":"Nummelin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6070-796X","authenticated-orcid":false,"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Non-clausal resolution and superposition with selection and redundancy criteria. In: Voronkov, A. (ed.) LPAR \u201992. LNCS, vol. 624, pp. 273\u2013284. Springer (1992)","DOI":"10.1007\/BFb0013068"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Backes, J., Brown, C.E.: Analytic tableaux for higher-order logic with choice. J. Autom. Reason. 47(4), 451\u2013479 (2011)","DOI":"10.1007\/s10817-011-9233-2"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) CADE-27. LNCS, vol. 11716, pp. 35\u201354. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, Springer (2021), to appear","DOI":"10.1007\/978-3-319-94205-6_3"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P., Waldmann, U.: Superposition with lambdas. J. Autom. Reason. To appear, preprint at https:\/\/arxiv.org\/abs\/2102.00453 (2021)","DOI":"10.1007\/s10817-021-09595-y"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J.C., Cruanes, S., Waldmann, U.: Superposition for lambda-free higher-order logic. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 28\u201346. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_3"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller, C., Sorge, V., Jamnik, M., Kerber, M.: Can a higher-order and a first-order theorem prover cooperate? In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 415\u2013431. Springer (2004)","DOI":"10.1007\/978-3-540-32275-7_27"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: Restricted combinatory unification. In: Fontaine, P. (ed.) CADE-27. LNCS, vol. 11716, pp. 74\u201393. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_5"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Bhayat, A., Reger, G.: A combinator-based superposition calculus for higher-order logic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I. LNCS, vol. 12166, pp. 278\u2013296. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_16"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Brown, C.E.: Reducing higher-order theorem proving to a sequence of SAT problems. J. Autom. Reason. 51(1), 57\u201377 (2013)","DOI":"10.1007\/s10817-013-9283-8"},{"key":"24_CR12","unstructured":"Cruanes, S.: Extending superposition with integer arithmetic, structural induction, and beyond. Ph.D. thesis, \u00c9cole polytechnique (2015)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Czajka, L., Kaliszyk, C.: Hammer for Coq: Automation for dependent type theory. J. Autom. Reason. 61(1\u20134), 423\u2013453 (2018)","DOI":"10.1007\/s10817-018-9458-4"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Denzinger, J., Kronenburg, M., Schulz, S.: DISCOUNT\u2013a distributed and learning equational prover. J. Autom. Reason. 18(2), 189\u2013198 (1997)","DOI":"10.1023\/A:1005879229581"},{"key":"24_CR15","unstructured":"Ebner, G., Blanchette, J., Tourret, S.: Unifying splitting. In: Platzer, A., Sutcliffe, G. (eds.) CADE-28. LNCS, Springer (2021), to appear"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"F\u00e4rber, M., Brown, C.E.: Internal guidance for Satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 349\u2013361. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_24"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3\u2013where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE-19. LNCS, vol. 2741, pp. 335\u2013349. Springer (2003)","DOI":"10.1007\/978-3-540-45085-6_31"},{"key":"24_CR19","doi-asserted-by":"crossref","unstructured":"Gleiss, B., Suda, M.: Layered clause selection for theory reasoning (short paper). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020, Part I. LNCS, vol. 12166, pp. 402\u2013409. Springer (2020)","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Hoder, K., Reger, G., Suda, M., Voronkov, A.: Selecting the selection. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 313\u2013329. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"24_CR21","doi-asserted-by":"crossref","unstructured":"Hoder, K., Voronkov, A.: Comparing unification algorithms in first-order theorem proving. In: Mertsching, B., Hund, M., Aziz, M.Z. (eds.) KI 2009. LNCS, vol. 5803, pp. 435\u2013443. Springer (2009)","DOI":"10.1007\/978-3-642-04617-9_55"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","DOI":"10.1016\/0304-3975(75)90011-0"},{"key":"24_CR23","doi-asserted-by":"crossref","unstructured":"Jensen, D.C., Pietrzykowski, T.: Mechanizing omega-order type theory through unification. Theor. Comput. Sci. 3(2), 123\u2013171 (1976)","DOI":"10.1016\/0304-3975(76)90021-9"},{"key":"24_CR24","doi-asserted-by":"crossref","unstructured":"Johnsson, T.: Lambda lifting: Transforming programs to recursive equations. In: Jouannaud, J. (ed.) FPCA 1985. LNCS, vol. 201, pp. 190\u2013203. Springer (1985)","DOI":"10.1007\/3-540-15975-4_37"},{"key":"24_CR25","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J.: HOL(y)Hammer: Online ATP service for HOL Light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","DOI":"10.1007\/s11786-014-0182-0"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"24_CR27","unstructured":"Kohlhase, M.: A mechanization of sorted higher-order logic based on the resolution principle. Ph.D. thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (1994)"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"24_CR29","unstructured":"Manna, Z., Waldinger, R.: A deductive approach to program synthesis. In: Buchanan, B.G. (ed.) IJCAI-79. pp. 542\u2013551. William Kaufmann (1979)"},{"key":"24_CR30","doi-asserted-by":"crossref","unstructured":"McCune, W., Wos, L.: Otter\u2013the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997)","DOI":"10.1023\/A:1005843632307"},{"key":"24_CR31","doi-asserted-by":"crossref","unstructured":"Murray, N.V.: Completely non-clausal theorem proving. Artif. Intell. 18(1), 67\u201385 (1982)","DOI":"10.1016\/0004-3702(82)90011-X"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Functional unification of higher-order patterns. In: Best, E. (ed.) LICS 1993. pp. 64\u201374. IEEE Computer Society (1993)","DOI":"10.1109\/LICS.1993.287599"},{"key":"24_CR33","doi-asserted-by":"crossref","unstructured":"Nonnengart, A., Weidenbach, C.: Computing small clause normal forms. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 335\u2013367. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"24_CR34","doi-asserted-by":"crossref","unstructured":"Okasaki, C.: Purely functional data structures. Cambridge University Press (1999)","DOI":"10.1017\/CBO9780511530104"},{"key":"24_CR35","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) IWIL-2010. EPiC Series in Computing, vol. 2, pp. 1\u201311. EasyChair (2010)"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 399\u2013415. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_28"},{"key":"24_CR37","unstructured":"Schulz, S.: E\u2013a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)"},{"key":"24_CR38","doi-asserted-by":"crossref","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE-27. LNCS, vol. 11716, pp. 495\u2013507. Springer (2019)","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"24_CR39","doi-asserted-by":"crossref","unstructured":"Schulz, S., M\u00f6hrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 330\u2013345. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"24_CR40","doi-asserted-by":"crossref","unstructured":"Steen, A.: Extensional paramodulation for higher-order logic and its effective implementation Leo-III. Ph.D. thesis, Free University of Berlin, Dahlem, Germany (2018)","DOI":"10.1007\/s13218-019-00628-8"},{"key":"24_CR41","doi-asserted-by":"crossref","unstructured":"Steen, A., Benzm\u00fcller, C.: There is no best $$\\beta $$-normalization strategy for higher-order reasoners. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR-20. LNCS, vol. 9450, pp. 329\u2013339. Springer (2015)","DOI":"10.1007\/978-3-662-48899-7_23"},{"key":"24_CR42","doi-asserted-by":"crossref","unstructured":"Steen, A., Benzm\u00fcller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS, vol. 10900, pp. 108\u2013116. Springer (2018)","DOI":"10.1007\/978-3-319-94205-6_8"},{"key":"24_CR43","doi-asserted-by":"crossref","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: A cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"24_CR44","doi-asserted-by":"crossref","unstructured":"Sultana, N., Blanchette, J.C., Paulson, L.C.: LEO-II and Satallax on the Sledgehammer test bench. J. Appl. Log. 11(1), 91\u2013102 (2013)","DOI":"10.1016\/j.jal.2012.12.002"},{"key":"24_CR45","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The CADE ATP System Competition\u2013CASC. AI Magazine 37(2), 99\u2013101 (2016)","DOI":"10.1609\/aimag.v37i2.2620"},{"key":"24_CR46","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure\u2013from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"24_CR47","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The CADE-27 automated theorem proving system competition\u2013CASC-27. AI Commun. 32(5-6), 373\u2013389 (2019)","DOI":"10.3233\/AIC-190627"},{"key":"24_CR48","doi-asserted-by":"crossref","unstructured":"Turner, D.A.: Another algorithm for bracket abstraction. J. Symb. Log. 44(2), 267\u2013270 (1979)","DOI":"10.2307\/2273733"},{"key":"24_CR49","doi-asserted-by":"crossref","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"24_CR50","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Blanchette, J.C., Cruanes, S., Schulz, S.: Extending a brainiac prover to lambda-free higher-order logic. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019, Part I. LNCS, vol. 11427, pp. 192\u2013210. Springer (2019)","DOI":"10.1007\/978-3-030-17462-0_11"},{"key":"24_CR51","unstructured":"Vukmirovi\u0107, P., Nummelin, V.: Boolean reasoning in a higher-order superposition prover. In: Fontaine, P., Korovin, K., Kotsireas, I.S., R\u00fcmmer, P., Tourret, S. (eds.) PAAR-2020. CEUR Workshop Proceedings, vol. 2752, pp. 148\u2013166. CEUR-WS.org (2020)"},{"key":"24_CR52","doi-asserted-by":"crossref","unstructured":"Vukmirovi\u0107, P., Bentkamp, A., Nummelin, V.: Efficient full higher-order unification. In: Ariola, Z.M. (ed.) FSCD. LIPIcs, vol. 167, pp. 5:1\u20135:17. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2020)","DOI":"10.46298\/lmcs-17(4:18)2021"},{"key":"24_CR53","doi-asserted-by":"crossref","unstructured":"Wisniewski, M., Steen, A., Kern, K., Benzm\u00fcller, C.: Effective normalization techniques for HOL. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS, vol. 9706, pp. 362\u2013370. Springer (2016)","DOI":"10.1007\/978-3-319-40229-1_25"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:31:03Z","timestamp":1672723863000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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","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","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}