2021/01/08 by Petros Papapanagiotou, Jacques Fleuriot
Computer Science · #Automated reasoning #Automated theorem proving #Formal Methods in Verification #HOL #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Monoidal t-norm logic #Natural deduction #Non-monotonic logic #Propositional calculus #Propositional variable #Sequent #Sequent calculus #T-norm fuzzy logics #cs.LO #cs.SC
paper · pdf · doi:10.4204/eptcs.332.2
published as EPTCS 332, 2021, pp. 18-34 · In Proceedings LFMTP 2020, arXiv:2101.02835
openalex publication_date 2021/01/08 · arxiv created 2021/01/11 · arxiv updated 2021/01/12 · openalex created_date 2021/01/18 · openalex updated_date 2026/08/05
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive forward and backward chaining in a sequent calculus style. It is made possible by automated machinery that take care of the necessary structural reasoning and term matching automatically. Our framework can also handle type theoretic correspondences of proofs, effectively allowing the type checking and construction of computational processes via proof. We demonstrate our implementation using a simple propositional logic and its Curry-Howard correspondence to the lambda-calculus, and argue its use with linear logic and its various correspondences to session types.