Files in this item



application/pdflin-chen-rosu-2021-tr.pdf (124kB)
Main articlePDF


Title:An Interactive Theorem Prover for Matching Logic with Proof Object Generation
Author(s):Lin, Zhengyao; Chen, Xiaohong; Rosu, Grigore
Subject(s):Interactive theorem prover
Matching logic
Abstract:Matching logic is a uniform logical foundation for K, which is a language semantics framework with the philosophy that all tooling around a language should be automatically generated from a single, rigorous definition of its formal semantics. In practice, K has been widely used to define the formal semantics of many real-world languages and to generate their execution and verification tools. However, there lacks a generic theorem prover that connects K with its logical foundation---matching logic. In this paper, we present ITP_ML, which is the first interactive theorem prover for matching logic. The main advantage of ITP_ML is its ability to generate machine-checkable proof objects as certificates that witness the correctness of its formal reasoning. ITP_ML is built on top of Metamath, a language to define formal systems, which allows it to have a small trust base of only 250 lines of code. ITP_ML supports both backward and forward proofs, allows users to dynamically add intermediate lemmas, and features automated proof tactics for common utilities such as reasoning about notations and proving propositional tautologies.
Issue Date:2021-10-04
Genre:Technical Report
Date Available in IDEALS:2021-10-05

This item appears in the following Collection(s)

Item Statistics