arXiv subjects

Laurenţiu Leuştean

Publications and source records attributed to Laurenţiu Leuştean.

6 recordsLinked to original sources

arXiv2025

Matching logic -- a new axiomatization

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.

cs.LO↗

arXiv2025

Notes on applicative matching logic

Matching logic (ML) was developed by Grigore Roşu and collaborators as a logic for defining the formal semantics of programming languages and for specifying and reasoning about the behavior of programs. These lecture notes present basic definitions and results on applicative matching logic (AML), a functional variant of ML introduced recently by Xiaohong Chen and Grigore Roşu. They can be used as an introductory text in the theory of AML. Monk's textbook on mathematical logic has an enormous influence on the notes.

cs.LO↗

arXiv2024

Proceedings Eighth Symposium on Working Formal Methods

The Working Formal Methods Symposium (FROM) is a series of workshops that aim to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or by creating or using software tools that apply theoretical contributions.

cs.LO↗

arXiv2024

Linear rates of asymptotic regularity for Halpern-type iterations

In this note we apply a lemma due to Sabach and Shtern to compute linear rates of asymptotic regularity for Halpern-type nonlinear iterations studied in optimization and nonlinear analysis.

math.OC↗

arXiv2023

Proceedings 7th Symposium on Working Formal Methods

This volume contains the proceedings of the 7th Working Formal Methods Symposium, which was held at the University of Bucharest, September 21-22, 2023.

cs.LO↗

arXiv2008

Maximal residuated lattices with lifting Boolean center

In this paper we define, inspired by ring theory, the class of maximal residuated lattices with lifting Boolean center and prove a structure theorem for them: any maximal residuated lattice with lifting Boolean center is isomorphic to a finite direct product of local residuated lattices.

math.LO↗