{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:05:51Z","timestamp":1746745551697,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"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>Subformula linking is an interactive theorem proving technique that was initially proposed for (classical) linear logic. It is based on truth and context preserving rewrites of a conjecture that are triggered by a user indicating<jats:italic>links<\/jats:italic>between subformulas, which can be done by direct manipulation, without the need of tactics or proof languages. The system guarantees that a true conjecture can always be rewritten to a known, usually trivial, theorem. In this work, we extend subformula linking to intuitionistic first-order logic with simply typed lambda-terms as the term language of this logic. We then use a well known embedding of intuitionistic type theory into this logic to demonstrate one way to extend linking to type theory.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_12","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"200-216","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Subformula Linking for Intuitionistic Logic with Application to Type Theory"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2938-547X","authenticated-orcid":false,"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"J.-M. Andreoli. Logic Programming with Focusing Proofs in Linear Logic. Journal of Logic and Computation, 2(3):297\u2013347, 1992$$.$$","DOI":"10.1093\/logcom\/2.3.297"},{"key":"12_CR2","unstructured":"D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang. Abella: A system for reasoning about relational specifications. Journal of Formalized Reasoning, 7(2), 2014$$.$$"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Y. Bertot, G. Kahn, and L. Th\u00e9ry. Proof by pointing. In Theoretical Aspects of Computer Software, pages 141\u2013160, 1994$$.$$","DOI":"10.1007\/3-540-57887-0_94"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"K.\u00a0Chaudhuri. Subformula linking as an interaction method. In S.\u00a0Blazy, C.\u00a0Paulin-Mohring, and D.\u00a0Pichardie, editors, 4th Conference on Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 386\u2013401. Springer, July 2013$$.$$","DOI":"10.1007\/978-3-642-39634-2_28"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"K. Chaudhuri, F. Pfenning, and G. Price. A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning, 40(2\u20133):133\u2013177, Mar. 2008$$.$$","DOI":"10.1007\/s10817-007-9091-0"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"A. Felty and D. Miller. Encoding a dependent-type $$\\lambda $$-calculus in a logic programming language. In CADE, volume 449 of LNAI, pages 221\u2013235. Springer, 1990$$.$$","DOI":"10.1007\/3-540-52885-7_90"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"A. Gacek, D. Miller, and G. Nadathur. A two-level logic approach to reasoning about computations. Journal of Automated Reasoning, 49(2):241\u2013273, 2012$$.$$","DOI":"10.1007\/s10817-011-9218-1"},{"key":"12_CR8","unstructured":"N. Guenot. Nested Deduction in Logical Foundations for Computation. Ph.d. thesis, Ecole Polytechnique, 2013$$.$$"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1993$$.$$","DOI":"10.1145\/138027.138060"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"C. Liang and D. Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747\u20134768, 2009$$.$$","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Negri, S., von Plato, J.: Structural Proof Theory. Cambridge University Press, 2001$$.$$","DOI":"10.1017\/CBO9780511527340"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. Higher-order abstract syntax. In ACM-SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 199\u2013208. ACM Press, June 1988$$.$$","DOI":"10.1145\/960116.54010"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"F.\u00a0Pfenning and C.\u00a0Sch\u00fcrmann. System description: Twelf \u2014 A meta-logical framework for deductive systems. In H.\u00a0Ganzinger, editor, 16th International Conference on Automated Deduction (CADE), number 1632 in LNAI, pages 202\u2013206, Trento, 1999. Springer$$.$$","DOI":"10.1007\/3-540-48660-7_14"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"B. C. Pierce and D. N. Turner. Local type inference. ACM Transactions of Programming Language Systems, 22(1):1\u201344, 2000$$.$$","DOI":"10.1145\/345099.345100"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Z. Snow, D. Baelde, and G. Nadathur. A meta-programming approach to realizing dependently typed logic programming. In Principles and Practices of Declarative Programming (PPDP), pages 187\u2013198, 2010$$.$$","DOI":"10.1145\/1836089.1836113"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"M. Southern. A Framework for Reasoning about LF Specifications. PhD thesis, University of Minnesota, Mar. 2021. Defended; final version to appear$$.$$","DOI":"10.4204\/EPTCS.337.8"},{"key":"12_CR17","unstructured":"L. Stra\u00dfburger. Linear Logic and Noncommutativity in the Calculus of Structures. PhD thesis, Technische Universit\u00e4t Dresden, 2003$$.$$"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"A.\u00a0Tiu. A local system for intuitionistic logic. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 4246 of LNCS, pages 242\u2013256. Springer, 2006$$.$$","DOI":"10.1007\/11916277_17"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework I: The propositional fragment. In Post-proceedings of TYPES 2003 Workshop, number 3085 in LNCS. Springer, 2003$$.$$","DOI":"10.21236\/ADA418510"}],"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_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:25:41Z","timestamp":1672723541000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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)"}}]}}