Article
Mathematics, Applied
John T. Baldwin, Viktor V. Verbovskiy
Summary: This article studies the strongly minimal M constructed by a 'Hrushovski construction', and shows that if the Hrushovski algebraization function μ belongs to a certain class T, then for independent I, dcl*(I) = 0. This implies that the only definable truly n-ary functions f occur when n = 1. It is also demonstrated that for Hrushovski's original construction and the strongly minimal k-Steiner systems of Baldwin and Paolini, the symmetric definable closure sdcl*(I) = ∅, indicating the impossibility of eliminating imaginaries.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Mathematics, Applied
M. Shahryari
Summary: This paper first presents an explicit description for the radicals of systems of equation over an algebra A and then proves an assertion using a new elementary argument. Furthermore, q(kappa)-compact algebras and kappa-filterpowers are defined, and the geometric equivalence between any q(kappa)-compact algebra and its kappa-filterpowers is shown. Unlike the classical argument, our proof still works even without an algebraic description of the kappa-quasivariety generated by an algebra.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Computer Science, Theory & Methods
Valentina Castiglioni, Ruggero Lanotte, Simone Tini
Summary: In probabilistic process algebras, quantitative information about process behavior is added to the classic qualitative description. Equivalence and distance between processes are checked using behavioral equivalences and metrics. Compositional reasoning relies on the preservation of equivalence and closeness under the application of language operators. SOS specification formats provide a convenient way to verify these compositional properties.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Mathematics, Applied
Sam van Gool, Jeremie Marques
Summary: This paper studies first-order coherent logic from the perspective of duality and categorical logic. It proves a duality theorem between coherent hyperdoctrines and open polyadic Priestley spaces, which is subsequently used to prove completeness, omitting types, and Craig interpolation theorems for coherent or intuitionistic logic. The approach emphasizes the importance of interpolation and openness properties and allows for a modular, syntax-free treatment of these model-theoretic results.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Mathematics, Applied
Radek Honzik, Chris Lambie-Hanson, Sarka Stejskalova
Summary: This paper shows that the Proper Forcing Axiom (PFA) has implications on the addition of Cohen subsets to w, in that it does not add specific types of trees (w2-Aronszajn trees and weak w1-Kurepa trees), and acentered forcing cannot add a weak w1-Kurepa tree. Furthermore, the paper studies variations of the principle GMP at higher cardinals and the indestructibility consequences they entail, addressing a question on weakly but not strongly inaccessible cardinals and proving the absence of weak aleph omega +1-Kurepa trees and aleph omega+2-Aronszajn trees in a model.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Computer Science, Theory & Methods
Jens Kosiol, Stefan John, Gabriele Taentzer
Summary: This paper presents a generic crossover construction for graph-like structures, which can be used to implement crossover operators for models in model-driven optimization. The construction allows for the generation of new solution models through graph transformations and provides a set of crossover operators for specific problems and situations on graphs.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Computer Science, Theory & Methods
Luc Edixhoven, Sung-Shik Jongmans, Jose Proenca, Ilaria Castellani
Summary: Choreographic languages describe sequences of interactions among agents, and pomsets provide a compact way to represent causality and concurrency. However, pomsets lack the ability to represent choices, so a set of pomsets is needed for branching behavior. This paper proposes branching pomsets, which can represent branching behavior using ordered actions. The paper compares branching pomsets with other event structures and shows their application in encoding choreographies.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Computer Science, Theory & Methods
Giacomo Maletto, Luca Roversi
Summary: In this article, reversible primitive permutations (RPP) are introduced as a class of recursive functions that model reversible computation. The authors present a proof, verified using the proof-assistant Lean, demonstrating that RPP can encode every primitive recursive function and that each RPP can be encoded as a primitive recursive function. The article also highlights a programming pattern for reversible algorithms and provides Lean source code for experimentations with certified properties of reversible computation.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Computer Science, Theory & Methods
D. Della Giustina, C. Londero, C. Piazza, B. Riccardi, R. Romanello
Summary: This paper introduces a novel high-level graph representation in quantum computation that supports dynamic connectivity typical of real-world network applications. It allows for encoding any multigraph into a unitary matrix and presents optimized algorithms for computing the encoding, demonstrating their effectiveness with examples. The paper also discusses how to react to edge/node failures in constant time and presents two methods for performing quantum random walks using this encoding.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Computer Science, Theory & Methods
Abdelkrim Abdelli
Summary: This paper explores a novel approach to construct an over-approximation of the state space of preemptive real-time systems. By extending the expression of a node to encode the time properties of past-fired subsequences, relevant time information is restored to improve computational efficiency.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Mathematics, Applied
Peter Nyikos, Lyubomyr Zdomskyy
Summary: In this paper, various conditions are given for a locally compact, omega(1)-compact space to be sigma-countably compact. Many of the results are independent of the usual (ZFC) axioms of set theory and may involve large cardinals. The paper also discusses unsolved problems and the use of set theoretic tools for consistency results.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Mathematics, Applied
Tomasz Weiss, Piotr Zakrzewski
Summary: This article studies a strengthening of the concepts of universally meager and universally null sets, introducing the notions of countably perfectly meager and countably perfectly null sets. The article proves the existence of universally meager and universally null sets that do not satisfy the properties of being countably perfectly meager and countably perfectly null, respectively, under certain conditions.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Computer Science, Theory & Methods
Francisco Duran, Nicolas Pozas, Camilo Rocha
Summary: This paper presents an approach for analyzing business process provisioning using a resource prediction strategy based on deep learning. It integrates a timed and probabilistic rewrite theory specification with a long short-term memory neural network as an external oracle. The approach includes comparison of execution time and resource occupancy under different parameters, as well as details on the construction of the deep learning model and its integration with Maude.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Mathematics, Applied
Nikolay Bazhenov, Marta Fiori-Carones, Lu Liu, Alexander Melnikov
Summary: This study investigates the proof-theoretic strength of theorems in countable algebra, analysis, and infinite combinatorics using the second-order analogy PRA2 of PRA, and compares the results with similar studies in primitive recursive algebra and analysis, as well as combinatorics. The researchers argue that PRA2 is robust enough to be an alternative base system for studying the proof-theoretic content of theorems in ordinary mathematics. The study discovers that many theorems known to be true in RCA0 also hold in PRA2 or are equivalent to RCA0 or its weaker analogy 2N-RCA0 over PRA2, but some standard mathematical and combinatorial facts are incomparable with these natural subsystems.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Mathematics, Applied
Igor Gorbunov, Dmitry Shkatov
Summary: This paper solves the problem of the existence of extensions of Solovay's system S that do not admit deductively independent sets of axioms by exhibiting countably many extensions of S without deductively independent sets of axioms.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Computer Science, Theory & Methods
Rodrigo Raya, Viktor Kuncak
Summary: This article introduces a methodology based on decomposition theorems to classify the theories handled by specialized decision procedures for automatic verification of programs manipulating arrays. It further applies this method to obtain an extension of combinatory array logic. The article also provides a classification of six different fragments based on their expressiveness.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Mathematics, Applied
Ur Ya'ar
Summary: We have proved the theory of constructing models using finitely many cofinality quantifiers - C*(lambda 1,...,lambda n) and C*(-closed sets.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Mathematics, Applied
Alexander I. Bufetov, Gabriel Nivasch, Fedor Pakhomov
Summary: This paper investigates the properties of fusible numbers and recursively defined functions, and explores the limitations of the order types of well-ordered sets generated by repeated application of functions.
ANNALS OF PURE AND APPLIED LOGIC
(2024)
Article
Computer Science, Theory & Methods
Clement Aubert
Summary: This article presents a general principle for checking the correctness of the definition of concurrency in concurrent calculi. It examines the use of reversibility in providing a criterion for assessing the correctness of concurrencies. The article introduces a syntactical definition of concurrency for CCSK and also shows the equivalence or refinement of this formalism to pre-existing definitions for reversible systems.
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
(2024)
Article
Computer Science, Theory & Methods
Reinhard Kahle, Isabel Oitavem, Paulo Guilherme Santos
Summary: We study the numeral forms of completeness and consistency for weak theories, including $\mathsf {S}<^>1_2$ and $\mathsf {EA}$. This exploration leads us to examine the derivability conditions required to establish these results, as well as present a weak form of Godel's Second Incompleteness Theorem without using 'provability implies provable provability'. Additionally, we introduce a provability predicate that satisfies the mentioned derivability condition for weak theories, and present a completeness result through consistency statements. Moreover, we provide characterizations of the provability predicates for which the numeral results hold, with $\mathsf {EA}$ as the surrounding theory, and offer results on functions that compute finitist consistency statements.
JOURNAL OF LOGIC AND COMPUTATION
(2023)
