{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T14:10:23Z","timestamp":1765116623687,"version":"3.46.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031995354"},{"type":"electronic","value":"9783031995361"}],"license":[{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,1]],"date-time":"2025-08-01T00:00:00Z","timestamp":1754006400000},"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":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-99536-1_18","type":"book-chapter","created":{"date-parts":[[2025,7,31]],"date-time":"2025-07-31T10:54:23Z","timestamp":1753959263000},"page":"293-308","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof Search in\u00a0Classical Propositional Logic with\u00a0Partial Proof Terms"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6348-5653","authenticated-orcid":false,"given":"Jos\u00e9","family":"Esp\u00edrito Santo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5352-4807","authenticated-orcid":false,"given":"Ana Catarina","family":"Sousa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,8,1]]},"reference":[{"issue":"3","key":"18_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1093\/logcom\/2.3.297","volume":"2","author":"J Andreoli","year":"1992","unstructured":"Andreoli, J.: Logic programming with focusing proofs in linear logic. J. Log. Comput. 2(3), 297\u2013347 (1992)","journal-title":"J. Log. Comput."},{"issue":"3","key":"18_CR2","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1017\/S0956796807006612","volume":"18","author":"ZM Ariola","year":"2008","unstructured":"Ariola, Z.M., Herbelin, H.: Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3), 373\u2013419 (2008)","journal-title":"J. Funct. Program."},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Curien, P., Herbelin, H.: The duality of computation. In: Odersky, M., Wadler, P. (eds.) Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP 2000), Montreal, Canada, September 18-21, 2000, pp. 233\u2013243. ACM (2000)","DOI":"10.1145\/351240.351262"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Danos, V., Joinet, J.B., Schellinx, H.: LKQ and LKT: sequent calculi for second order logic based upon dual decompositions of classical implication. In: Girard, J.Y. (ed.) Advances in Linear Logic, pp. 211\u2013224. Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511629150.011"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Dunfield, J., Krishnaswami, N.: Bidirectional typing. ACM Comput. Surv. 54(5), 98:1\u201398:38 (2022)","DOI":"10.1145\/3450952"},{"issue":"1","key":"18_CR6","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1005099619660","volume":"60","author":"R Dyckhoff","year":"1998","unstructured":"Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Stud. Logica. 60(1), 107\u2013118 (1998)","journal-title":"Stud. Logica."},{"issue":"6","key":"18_CR7","doi-asserted-by":"publisher","first-page":"618","DOI":"10.1016\/j.apal.2012.05.008","volume":"164","author":"J Esp\u00edrito Santo","year":"2013","unstructured":"Esp\u00edrito Santo, J.: Towards a canonical classical natural deduction system. Ann. Pure Appl. Log. 164(6), 618\u2013650 (2013)","journal-title":"Ann. Pure Appl. Log."},{"issue":"1\u20133","key":"18_CR8","doi-asserted-by":"publisher","first-page":"111","DOI":"10.3233\/FI-2019-1857","volume":"170","author":"J Esp\u00edrito Santo","year":"2019","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Decidability of several concepts of finiteness for simple types. Fundam. Inform. 170(1\u20133), 111\u2013138 (2019)","journal-title":"Fundam. Inform."},{"issue":"8","key":"18_CR9","doi-asserted-by":"publisher","first-page":"1092","DOI":"10.1017\/S0960129518000099","volume":"29","author":"J Esp\u00edrito Santo","year":"2019","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search. Math. Struct. Comput. Sci. 29(8), 1092\u20131124 (2019)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"10","key":"18_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2021.103026","volume":"172","author":"J Esp\u00edrito Santo","year":"2021","unstructured":"Esp\u00edrito Santo, J., Matthes, R., Pinto, L.: A coinductive approach to proof search through typed lambda-calculi. Ann. Pure Appl. Logic 172(10), 103026 (2021)","journal-title":"Ann. Pure Appl. Logic"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-45793-3_36","volume-title":"Computer Science Logic","author":"H Geuvers","year":"2002","unstructured":"Geuvers, H., Jojgov, G.I.: Open proofs and open terms: a basis for interactive logic. In: Bradfield, J. (ed.) CSL 2002. LNCS, vol. 2471, pp. 537\u2013552. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45793-3_36"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0022247","volume-title":"Computer Science Logic","author":"H Herbelin","year":"1995","unstructured":"Herbelin, H.: A $$\\lambda $$-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 61\u201375. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/BFb0022247"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logic. Theor. Comput. Sci. 410, 4747\u20134768 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"18_CR14","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1017\/S0960129500003261","volume":"11","author":"CA Mu\u00f1oz","year":"2001","unstructured":"Mu\u00f1oz, C.A.: Dependent types and explicit substitutions: a meta-theoretical development. Math. Struct. Comput. Sci. 11(1), 91\u2013129 (2001)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1\u20132","key":"18_CR15","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1016\/S0304-3975(00)00196-1","volume":"266","author":"CA Mu\u00f1oz","year":"2001","unstructured":"Mu\u00f1oz, C.A.: Proof-term synthesis on dependent-type systems via explicit substitutions. Theor. Comput. Sci. 266(1\u20132), 407\u2013440 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Pfenning, F., Pientka, B.: Contextual modal type theory. ACM Trans. Comput. Log. 9(3), 23:1\u201323:49 (2008)","DOI":"10.1145\/1352582.1352591"},{"key":"18_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100827","volume":"130","author":"C Olarte","year":"2023","unstructured":"Olarte, C., Pimentel, E., Rocha, C.: A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems. J. Log. Algebraic Methods Program. 130, 100827 (2023)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/BFb0013061","volume-title":"Logic Programming and Automated Reasoning","author":"M Parigot","year":"1992","unstructured":"Parigot, M.: Lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190\u2013201. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/BFb0013061"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Esp\u00edrito Santo, J., Sousa, A.C.: Partial proof terms in the study of idealized proof search. In: Kohlhase, A., Kov\u00e1cs, L. (eds.) Intelligent Computer Mathematics - 17th International Conference, CICM 2024, Montr\u00e9al. LNCS, vol. 14960, pp. 279\u2013297. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-66997-2_16","DOI":"10.1007\/978-3-031-66997-2_16"},{"issue":"1","key":"18_CR20","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1023\/A:1005091418752","volume":"60","author":"W Sieg","year":"1998","unstructured":"Sieg, W., Byrnes, J.: Normal natural deduction proofs (in classical logic). Stud. Logica. 60(1), 67\u2013106 (1998)","journal-title":"Stud. Logica."},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-32254-2_11","volume-title":"Mechanizing Mathematical Reasoning","author":"W Sieg","year":"2005","unstructured":"Sieg, W., Cittadini, S.: Normal natural deduction proofs (in non-classical logics). In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 169\u2013191. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32254-2_11"}],"container-title":["Lecture Notes in Computer Science","Logic, Language, Information, and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99536-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,7]],"date-time":"2025-12-07T14:07:06Z","timestamp":1765116426000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99536-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,1]]},"ISBN":["9783031995354","9783031995361"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99536-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,8,1]]},"assertion":[{"value":"1 August 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"WoLLIC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Logic, Language, Information, and Computation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wollic2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/wollic.org\/wollic2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}