An Interactive Theorem Prover for Matching Logic with Proof Object Generation

Lin, Zhengyao; Chen, Xiaohong; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/111650 Copy

Description

Title

An Interactive Theorem Prover for Matching Logic with Proof Object Generation

Author(s)

• Lin, Zhengyao
• Chen, Xiaohong
• Rosu, Grigore

Issue Date

2021-10-04

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/111650

Owning Collections