Showing 1–3 of 3 results for author: Prunescu, M

A Minimal Substitution Basis for the Kalmar Elementary Functions

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

Abstract: We show that the class of Kalmar elementary functions can be inductively generated from the addition, the integer remainder and the base-two exponentiation, hence improving previous results by Marchenkov and Mazzanti. In addition, we further prove that the substitution basis defined by these three operations is minimal. We show that the class of Kalmar elementary functions can be inductively generated from the addition, the integer remainder and the base-two exponentiation, hence improving previous results by Marchenkov and Mazzanti. In addition, we further prove that the substitution basis defined by these three operations is minimal. △ Less

Submitted 24 May, 2025; originally announced May 2025.

MSC Class: 03D20 (Primary); 03D55; 03B70; 68Q15 (Secondary)

Symmetric Functions over Finite Fields

Authors: Mihai Prunescu

Abstract: The number of linear independent algebraic relations among elementary symmetric polynomial functions over finite fields is computed. An algorithm able to find all such relations is described. It is proved that the basis of the ideal of algebraic relations found by the algorithm consists of polynomials having coefficients in the prime field F_p. The number of linear independent algebraic relations among elementary symmetric polynomial functions over finite fields is computed. An algorithm able to find all such relations is described. It is proved that the basis of the ideal of algebraic relations found by the algorithm consists of polynomials having coefficients in the prime field F_p. △ Less

Submitted 24 September, 2023; originally announced September 2023.

Comments: In Proceedings FROM 2023, arXiv:2309.12959

ACM Class: I.1.2

Journal ref: EPTCS 389, 2023, pp. 131-143

Using Z3 to Verify Inferences in Fragments of Linear Logic

Authors: Alen Docef, Radu Negulescu, Mihai Prunescu

Abstract: Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic sequents that supports verification of logic inference rules using automatic theorem proving. Specifically, we use the Z3 Theorem Prover [8] to check targeted infe… ▽ More Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic sequents that supports verification of logic inference rules using automatic theorem proving. Specifically, we use the Z3 Theorem Prover [8] to check targeted inference rules based on a set of inference rules that are presumed to be valid. To demonstrate the approach, we apply it to validate several derived inference rules for two different fragments of linear logic: MLL+Mix (Multiplicative Linear Logic extended with a Mix rule) and MILL (Multiplicative Intuitionistic Linear Logic). △ Less

Submitted 24 September, 2023; originally announced September 2023.

Comments: In Proceedings FROM 2023, arXiv:2309.12959

ACM Class: F.4.1; I.2.3

Journal ref: EPTCS 389, 2023, pp. 11-25