An Interactive Theorem Prover for Matching Logic with Proof Object Generation
Zhengyao Lin, Xiaohong Chen, Grigore Roşu · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 2021
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.