3 papers
cs.LO2025
Matching logic -- a new axiomatization
Laurenţiu Leuştean, Dafina Trufaş
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 f…
cs.LO2024
Intuitionistic Propositional Logic in Lean
Dafina Trufaş
In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studie…
cs.LO2023
Asynchronous Muddy Children Puzzle (work in progress)
Dafina Trufaş, Ioan Teodorescu, Denisa Diaconescu +2
In this work-in-progress paper we explore using the recently introduced VLSM formalism to define and reason about the dynamics of agent-based systems. To this aim we use VLSMs to f…