https://arxiv.org/api/XJAGxHw0Q+K0PfE0LdWUGG3MHvA 2026-06-14T12:06:49Z 3138 345 15 http://arxiv.org/abs/2508.02918v1 2025-08-04T21:48:47Z

We study central configurations when the set of positions is symmetric. We use a theorem from representation theory of finite groups to explore the symmetry properties of equations for central configurations. This approach simplifies equations for central configurations by considering arbitrary numbers of bodies, symmetry groups, and dimensions. We discuss how to use this theorem to obtain a more refined decomposition of the equations than that given before. The decomposition presented here uses the symmetry-adapted basis method. As an application, we give a complete description of the existence and which masses are possible for central configurations of two nested regular tetrahedrons, two nested regular octahedrons, and two nested regular cubes. To do this, we employ some methods of rational parameterizations and isolation of zeros of multivariate polynomials. The decomposition obtained allows symbolic calculations to be used to study the expressions. This way, we summarize previous discussions and extend them by completing the analysis on the cube case, for both the inverse and direct problems.

2025-08-04T21:48:47Z Marcelo P. Santos Federal Rural University of Pernambuco Leon D. da Silva Federal Rural University of Pernambuco http://arxiv.org/abs/2508.00153v2 2025-08-04T03:57:25Z

Green computing represents a critical pathway to decarbonize the digital economy while maintaining technological progress. This article examines how sustainable IT strategies including energy-efficient hardware, AI-optimized data centres, and circular e-waste systems can transform computing into a net carbon sink. Through analysis of industry best practices and emerging technologies like quantum computing and biodegradable electronics, we demonstrate achievable reductions of 40-60% in energy consumption without compromising performance. The study highlights three key findings: (1) current solutions already deliver both environmental and economic benefits, with typical payback periods of 3-5 years; (2) systemic barriers including cost premiums and policy fragmentation require coordinated action; and (3) next-generation innovations promise order-of-magnitude improvements in efficiency. We present a practical framework for stakeholders from corporations adopting renewable-powered cloud services to individuals extending device lifespans to accelerate the transition. The research underscores computing's unique potential as a climate solution through its rapid innovation cycles and measurable impacts, concluding that strategic investments in green IT today can yield disproportionate sustainability dividends across all sectors tomorrow. This work provides both a compelling case for urgent action and a clear roadmap to realize computing's potential as a powerful carbon destruction tool in the climate crisis era.

2025-07-31T20:28:29Z 26 Pages, 6 Tables Sayed Mahbub Hasan Amiri Prasun Goswami Md. Mainul Islam Mohammad Shakhawat Hossen Marzana Mithila Naznin Akter http://arxiv.org/abs/2201.07127v3 2025-08-03T03:48:42Z

Let $(u(n))_{n\in\mathbb{N}}$ be an arithmetic progression of natural integers in base $b\in\mathbb{N}\setminus \{0,1\}$. We consider the following sequences: $s(n)=\overline{u(0)u(1)\cdots u(n) }^b$ formed by concatenating the first $n+1$ terms of $(u(n))_{n\in\mathbb{N}}$ in base $b$ from the right; $s_g(n) = \overline{u(n)u(n-1)\cdots u(0)}^b$; and $(s_*(n))_{n\in\mathbb{N}}$, given by $s_*(0)=u(0)$, $s_*(n)=\overline{s(n)s_g(n-1)}^b, n\geq 1$. We construct explicit formulae for these sequences and use basic concepts of linear difference operators to prove they are not P-recursive (holonomic). We also present an alternative proof that follows directly from their definitions. We implemented $(s(n))_{n\in\mathbb{N}}$ and $(s_g(n))_{n\in\mathbb{N}}$ in the decimal base when $(u(n))_{n\in\mathbb{N}}=\mathbb{N}\setminus \{0\}$.

2022-01-14T07:53:47Z Definitions 1, 2, and 3 are new. More details about "holonomicity per range'' have been added Florian Luca Bertrand Teguia Tabuguia http://arxiv.org/abs/2508.00512v1 2025-08-01T10:45:24Z

The cylindrical algebraic decomposition (CAD) is the only complete method used in practice for solving problems like quantifier elimination or SMT solving related to real algebra, despite its doubly exponential complexity. Recent exploration-guided algorithms like NLSAT, NuCAD, and CAlC rely on CAD technology but reduce the computational effort heuristically. Single cell construction is a paradigm that is used in each of these algorithms. The central property on which the CAD algorithm is based is called delineability. Recently, we introduced a weaker notion called projective delineability which can require fewer computations to guarantee, but needs to be applied carefully. This paper adapts the single cell construction for exploiting projective delineability and reports on experimental results.

2025-08-01T10:45:24Z Jasper Nalbach Lucas Michel Erika Ábrahám Christopher W. Brown James H. Davenport Matthew England Pierre Mathonet Naïm Zénaïdi http://arxiv.org/abs/2508.00505v1 2025-08-01T10:33:03Z

The Cylindrical Algebraic Decomposition (CAD) method is currently the only complete algorithm used in practice for solving real-algebraic problems. To ameliorate its doubly-exponential complexity, different exploration-guided adaptations try to avoid some of the computations. The first such adaptation named NLSAT was followed by Non-uniform CAD (NuCAD) and the Cylindrical Algebraic Covering (CAlC). Both NLSAT and CAlC have been developed and implemented in SMT solvers for satisfiability checking, and CAlC was recently also adapted for quantifier elimination. However, NuCAD was designed for quantifier elimination only, and no complete implementation existed before this work. In this paper, we present a novel variant of NuCAD for both real quantifier elimination and SMT solving, provide an implementation, and evaluate the method by experimentally comparing it to CAlC.

2025-08-01T10:33:03Z Jasper Nalbach Erika Ábrahám http://arxiv.org/abs/2507.23557v1 2025-07-31T13:46:17Z

We consider a family of infinite sums of products of Catalan numbers, indexed by trees. We show that these sums are polynomials in $1/π$ with rational coefficients; the proof is effective and provides an algorithm to explicitly compute these sums. Along the way we introduce parametric liftings of our sums, and show that they are polynomials in the complete elliptic integrals of the first and second kind. Moreover, the degrees of these polynomials are at most half of the number of vertices of the tree. The computation of these tree-indexed sums is motivated by the study of large meandric systems, which are non-crossing configurations of loops in the plane.

2025-07-31T13:46:17Z 62 pages, 8 figures Alin Bostan Valentin Féray Paul Thévenin http://arxiv.org/abs/2507.22255v1 2025-07-29T22:09:35Z

The pursuit of general intelligence has traditionally centered on external objectives: an agent's control over its environments or mastery of specific tasks. This external focus, however, can produce specialized agents that lack adaptability. We propose representational empowerment, a new perspective towards a truly agent-centric learning paradigm by moving the locus of control inward. This objective measures an agent's ability to controllably maintain and diversify its own knowledge structures. We posit that the capacity -- to shape one's own understanding -- is an element for achieving better ``preparedness'' distinct from direct environmental influence. Focusing on internal representations as the main substrate for computing empowerment offers a new lens through which to design adaptable intelligent systems.

2025-07-29T22:09:35Z RLC Finding the Frame Workshop 2025 Hanqi Zhou Fryderyk Mantiuk David G. Nagy Charley M. Wu http://arxiv.org/abs/2507.20889v1 2025-07-28T14:40:07Z

In 1978, Frost and Storey asserted that a bivariate polynomial matrix is equivalent to its Smith normal form if and only if the reduced minors of all orders generate the unit ideal. In this paper, we first demonstrate by constructing an example that for any given positive integer s with s >= 2, there exists a square bivariate polynomial matrix M with the degree of det(M) in y equal to s, for which the condition that reduced minors of all orders generate the unit ideal is not a sufficient condition for M to be equivalent to its Smith normal form. Subsequently, we prove that for any square bivariate polynomial matrix M where the degree of det(M) in y is at most 1, Frost and Storey's assertion holds. Using the Quillen-Suslin theorem, we further extend our consideration of M to rank-deficient and non-square cases.

2025-07-28T14:40:07Z 16 pages Dong Lu Dingkang Wang Fanghui Xiao Xiaopeng Zheng http://arxiv.org/abs/2507.20491v1 2025-07-28T03:00:35Z

Recent advances in large language models (LLMs) have significantly enhanced question-answering (QA) capabilities, particularly in open-domain contexts. However, in closed-domain scenarios such as education, healthcare, and law, users demand not only accurate answers but also transparent reasoning and explainable decision-making processes. While neural-symbolic (NeSy) frameworks have emerged as a promising solution, leveraging LLMs for natural language understanding and symbolic systems for formal reasoning, existing approaches often rely on large-scale models and exhibit inefficiencies in translating natural language into formal logic representations. To address these limitations, we introduce Text-JEPA (Text-based Joint-Embedding Predictive Architecture), a lightweight yet effective framework for converting natural language into first-order logic (NL2FOL). Drawing inspiration from dual-system cognitive theory, Text-JEPA emulates System 1 by efficiently generating logic representations, while the Z3 solver operates as System 2, enabling robust logical inference. To rigorously evaluate the NL2FOL-to-reasoning pipeline, we propose a comprehensive evaluation framework comprising three custom metrics: conversion score, reasoning score, and Spearman rho score, which collectively capture the quality of logical translation and its downstream impact on reasoning accuracy. Empirical results on domain-specific datasets demonstrate that Text-JEPA achieves competitive performance with significantly lower computational overhead compared to larger LLM-based systems. Our findings highlight the potential of structured, interpretable reasoning frameworks for building efficient and explainable QA systems in specialized domains.

2025-07-28T03:00:35Z 8 pages, 3 figures. Accepted at the International Joint Conference on Neural Networks (IJCNN) 2025, Workshop on Trustworthiness and Reliability in Neuro-Symbolic AI. https://2025.ijcnn.org Tuan Bui Trong Le Phat Thai Sang Nguyen Minh Hua Ngan Pham Thang Bui Tho Quan http://arxiv.org/abs/2507.20267v1 2025-07-27T13:27:20Z

Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for different sets of variables, which leads to unnecessarily large proofs. To overcome this issue we extend the existing Practical Algebraic Calculus with linear combinations (LPAC) with two new proof rules that allow us to capture and reuse parts of the proof to derive a more condensed proof certificate. We integrate these rules into the proof checker Pacheck 2.0. Our experimental results demonstrate that the proposed extension helps to reduce both proof size and verification time.

2025-07-27T13:27:20Z 6 pages; 2 figures; 1 table Daniela Kaufmann Clemens Hofstadler http://arxiv.org/abs/2501.03837v2 2025-07-27T04:03:09Z

We adapt the theory of normal and special polynomials from symbolic integration to the summation setting, and then built up a general framework embracing both the usual shift case and the $q$-shift case. In the context of this general framework, we develop a unified reduction algorithm, and subsequently a creative telescoping algorithm, applicable to both hypergeometric terms and their $q$-analogues. Our algorithms allow to split up the usual shift case and the $q$-shift case only when it is really necessary, and thus instantly reveal the intrinsic differences between these two cases. Computational experiments are also provided.

2025-01-07T14:47:02Z Shaoshi Chen Hao Du Yiman Gao Hui Huang Ziming Li 10.1007/s11139-025-01164-w http://arxiv.org/abs/2507.19010v1 2025-07-25T07:07:28Z

We present an experimental, verified clause processor ctv-cp that fits into the framework used at Arm for formal verification of arithmetic hardware designs. This largely automates the ACL2 proof development effort for integer multiplier modules that exist in designs ranging from floating-point division to matrix multiplication.

2025-07-25T07:07:28Z In Proceedings ACL2 2025, arXiv:2507.18567 EPTCS 423, 2025, pp. 51-55 Mayank Manjrekar Arm Inc. 10.4204/EPTCS.423.5 http://arxiv.org/abs/2507.15449v1 2025-07-21T10:01:42Z

We consider the multivariate scheme Pesto, which was introduced by Calderini, Caminata, and Villa. In this scheme, the public polynomials are obtained by applying a CCZ transformation to a set of quadratic secret polynomials. As a consequence, the public key consists of polynomials of degree 4. In this work, we show that the public degree 4 polynomial system can be efficiently reduced to a system of quadratic polynomials. This seems to suggest that the CCZ transformation may not offer a significant increase in security, contrary to what was initially believed.

2025-07-21T10:01:42Z are welcome! Alessio Caminata Elisa Gorla Madison Mabe Martina Vigorito Irene Villa http://arxiv.org/abs/2502.12721v2 2025-07-21T08:13:58Z

The MinRank problem is a simple linear algebra problem: given matrices with coefficients in a field, find a non trivial linear combination of the matrices that has a small rank. There are several algebraic modeling of the problem. The main ones are: the Kipnis-Shamir modeling, the Minors modeling and the Support-Minors modeling. The Minors modeling has been studied by Faug{è}re et al. in 2010, where the authors provide an analysis of the complexity of computing a Gr{ö}bner basis of the modeling, through the computation of the exact Hilbert Series for a generic instance. For the Support-Minors modeling, the first terms of the Hilbert Series are given by Bardet et al. in 2020 based on an heuristic and experimental work. In this work, we provide a formula and a proof for the complete Hilbert Series of the Support Minors modeling for generic instances. This is done by adapting well known results on determinantal ideals to an ideal generated by a particular subset of the set of all minors of a matrix of variables. We then show that this ideal is generated by

2025-02-18T10:38:06Z Magali Bardet CA - LITIS Alban Gilard CA - LITIS http://arxiv.org/abs/2306.15375v2 2025-07-18T07:57:21Z

We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library's dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.

2023-06-27T10:47:22Z Proc. ACM Program. Lang. 9, ICFP, Article 237 (August 2025), 36 pages Guillaume Allais Edwin Brady Nathan Corbyn Ohad Kammar Jeremy Yallop 10.1145/3747506