TY - GEN
T1 - Subformula Linking for Intuitionistic Logic with Application to Type Theory
AU - Chaudhuri, Kaustuv
N1 - Publisher Copyright:
© 2021, The Author(s).
PY - 2021/1/1
Y1 - 2021/1/1
N2 - 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 links 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.
AB - 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 links 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.
UR - https://www.scopus.com/pages/publications/85112341069
U2 - 10.1007/978-3-030-79876-5_12
DO - 10.1007/978-3-030-79876-5_12
M3 - Conference contribution
AN - SCOPUS:85112341069
SN - 9783030798758
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 200
EP - 216
BT - Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings
A2 - Platzer, André
A2 - Sutcliffe, Geoff
PB - Springer Science and Business Media Deutschland GmbH
T2 - 28th International Conference on Automated Deduction, CADE 28 2021
Y2 - 12 July 2021 through 15 July 2021
ER -