Summary
Sometimes, computers need to reason using logic that avoids assuming things without proof, called intuitionistic logic. The authors work on a version of matching logic that fits this constructive style. They created a way to interpret this logic using mathematical structures called complete Heyting algebras. They also designed a system to prove statements in this logic and showed it works correctly according to their interpretation.
What this means in practice
- •For program verification teams: Use intuitionistic matching logic semantics to build proof systems that ensure program correctness without classical assumptions.
- •For formal methods engineers: Implement logic frameworks with complete Heyting algebra semantics to support reasoning in constructive verification workflows.
A theory result. No direct application yet.
Abstract
We present work in progress towards an intuitionistic version of Applicative Matching Logic. We introduce a semantics based on complete Heyting algebras, and propose a proof system which we prove to be sound relative to this semantics.