activity
20232026
most citedUsing Z3 to Verify Inferences in Fragments of Linear Logic

1 citations · 1 across the 14 of their papers we have counts for

collaborators
Showing math.LOShow all

6 papers · 1 filter

math.LO2026

Undecidability, Chaos and Universality in Arithmetic Terms

Gabriel Istrate, Mihai Prunescu, Joseph M. Shunia

Arithmetic terms are finite fixed compositions of additions, subtractions, multiplications, divisions with remainder and exponentiations, containing variables interpreted as natura…

math.LO2025

On polynomial systems of equations in square matrices filled with natural numbers

Mihai Prunescu

The positive existential theories of the sets without parameters build an inclusion lattice isomorhic with the lattice of divisibility. All these sets are algorith…

math.LO2025

On the first-order theory of the remainder

Mihai Prunescu

It is proved that the first-order theory of the structure (N,mod) is undecidable. Here mod denotes the operation of computing the remainder for any division between positive intege…

math.LO2025

Proof verification by polynomial Fingerprinting

Mihai Prunescu

To cater to the needs of fast verification for mathematical proofs, we describe a method to encode formal sentences in - matrices over multivariate polynomials with in…

math.LO2025

A Minimal Substitution Basis for the Kalmár Elementary Functions

Mihai Prunescu, Lorenzo Sauras-Altuzarra, Joseph M. Shunia

We show that the class of Kalmár elementary functions can be inductively generated from the addition, the integer remainder, and the base-two exponentiation, hence improving previo…

math.LO2024

On the representation of C-recursive integer sequences by arithmetic terms

Mihai Prunescu, Lorenzo Sauras-Altuzarra

We show that, if an integer sequence is given by a linear recurrence of constant rational coefficients, then it can be represented as the difference of two arithmetic terms with ex…