TY - GEN
T1 - A system of inference based on proof search
T2 - 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023
AU - Miller, Dale
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023/1/1
Y1 - 2023/1/1
N2 - Gentzen designed his natural deduction proof system to "come as close as possible to actual reasoning."Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.
AB - Gentzen designed his natural deduction proof system to "come as close as possible to actual reasoning."Indeed, natural deduction proofs closely resemble the static structure of logical reasoning in mathematical arguments. However, different features of inference are compelling to capture when one wants to support the process of searching for proofs. PSF (Proof Search Framework) attempts to capture these features naturally and directly. The design and metatheory of PSF are presented, and its ability to specify a range of proof systems for classical, intuitionistic, and linear logic is illustrated.
KW - logical frameworks
KW - proof search
KW - proof systems
U2 - 10.1109/LICS56636.2023.10175827
DO - 10.1109/LICS56636.2023.10175827
M3 - Conference contribution
AN - SCOPUS:85166002979
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 26 June 2023 through 29 June 2023
ER -