Matching logic -- a new axiomatization

2025/06/13 by Laurenţiu Leuştean, Leuştean, Laurenţiu, Dafina Trufaş +1
Computer Science · #03B70 #68Q55 #F.3.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Semantic Web and Ontologies

paper · pdf · doi:10.48550/arxiv.2506.13801

openalex publication_date 2025/06/13 · openalex created_date 2025/10/09 · openalex updated_date 2026/07/28

Abstract

In these notes we propose a new, simpler proof system for first-order matching logic with application and definedness. The new proof system is inspired by Tarski's axiomatization for first order-logic with equality (simplified by Kalish and Montague), that does not involve the notions of a free variable and free substitution. We give also a proof system for first-order matching logic with application, obtained by adapting to matching logic Gödel's proof system for first-order intuitionistic logic.

Related

• Notes on applicative matching logic
• On a Dependently Typed Encoding of Matching Logic
• Completeness proof of functional logic, a formalism with\n variable-binding nonlogical symbols
• Tarski's relevance logic; Version 2
• Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)