https://arxiv.org/api/z8yzDNxxLctfZCHcSv+zTMk9sHQ 2026-06-15T01:29:18Z 3138 540 15 http://arxiv.org/abs/2312.16210v2 2024-12-26T21:53:05Z

This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of symbolic computation and were first implemented in computer algebra systems decades ago, but have recently received renewed interest as part of the ongoing development of SMT solvers for non-linear real arithmetic. First, we consider the use of iterated univariate resultants in traditional CAD, and how this leads to inefficiencies, especially in the case of an input with multiple equational constraints. We reproduce the workshop paper [Davenport and England, 2023], adding important clarifications to our suggestions first made there to make use of multivariate resultants in the projection phase of CAD. We then consider an alternative approach to this problem first documented in [McCallum and Brown, 2009] which redefines the actual object under construction, albeit only in the case of two equational constraints. We correct an unhelpful typo and provide a proof missing from that paper. We finish by revising the topic of how to deal with SMT or Real QE problems expressed using rational functions (as opposed to the usual polynomial ones) noting that these are often found in industrial applications. We revisit a proposal made in [Uncu, Davenport and England, 2023] for doing this in the case of satisfiability, explaining why such an approach does not trivially extend to more complicated quantification structure and giving a suitable alternative.

2023-12-23T17:32:45Z Submitted to Mathematics in Computer Science Mathematics in Computer Science, volume 19, article number 12, Springer, 2025 James H. Davenport Matthew England Scott McCallum Ali K. Uncu 10.1007/s11786-025-00606-4 http://arxiv.org/abs/2412.19287v1 2024-12-26T17:19:56Z

In this work, we introduce a semi-algebraic model for automatic parallelization of perfectly nested polynomial loops, which generalizes the classical polyhedral model. This model supports the basic tasks for automatic loop parallelization, such as the representation of the nested loop, the dependence analysis, the computation of valid schedules, as well as the transformation of the loop program with a valid schedule.

2024-12-26T17:19:56Z Changbo Chen http://arxiv.org/abs/2412.18294v1 2024-12-24T09:02:57Z

This paper presents an advanced method for addressing the inverse kinematics and optimal path planning challenges in robot manipulators. The inverse kinematics problem involves determining the joint angles for a given position and orientation of the end-effector. Furthermore, the path planning problem seeks a trajectory between two points. Traditional approaches in computer algebra have utilized Gröbner basis computations to solve these problems, offering a global solution but at a high computational cost. To overcome the issue, the present authors have proposed a novel approach that employs the Comprehensive Gröbner System (CGS) and CGS-based quantifier elimination (CGS-QE) methods to efficiently solve the inverse kinematics problem and certify the existence of solutions for trajectory planning. This paper extends these methods by incorporating smooth curves via cubic spline interpolation for path planning and optimizing joint configurations using shortest path algorithms to minimize the sum of joint configurations along a trajectory. This approach significantly enhances the manipulator's ability to navigate complex paths and optimize movement sequences.

2024-12-24T09:02:57Z 16 pages Yusuke Shirato Natsumi Oka Akira Terui Masahiko Mikawa http://arxiv.org/abs/2412.18143v1 2024-12-24T03:55:24Z

Graphs are the most suitable structures for modeling objects and interactions in applications where component inter-connectivity is a key feature. There has been increased interest in graphs to represent domains such as social networks, web site link structures, and biology. Graph stores recently rose to prominence along the NoSQL movement. In this work we will focus on NOSQL graph databases, describing their peculiarities that sets them apart from other data storage and management solutions, and how they differ among themselves. We will also analyze in-depth two different graph database management systems - AllegroGraph and Neo4j that uses the most popular graph models used by NoSQL stores in practice: the resource description framework (RDF) and the labeled property graph (LPG), respectively.

2024-12-24T03:55:24Z Monografias em Ciência da Computação, PUC-Rio Veronica Santos Bruno Cuconato http://arxiv.org/abs/2412.17280v1 2024-12-23T05:03:13Z

This study presents a comprehensive mathematical framework for modeling the flight dynamics of a six-degree-of-freedom fixed-wing aircraft as a rigid body with three control surfaces: rudder, elevators, and ailerons. The framework consists of 35 differential-algebraic equations (DAEs) and requires 30 constants to be specified. It supports both direct and inverse flight dynamics analyses. In direct dynamics, the historical profiles of control inputs (deflection angles and engine thrust) are specified, and the resulting flight trajectory is predicted. In inverse dynamics, the desired flight trajectory and an additional constraint are specified to determine the required control inputs. The framework employs wind axes for linear-momentum equations and body axes for angular-momentum equations, incorporates two flight path angles, and provides formulas for aerodynamic force and moment coefficients. Key advantages include improved computational efficiency, elimination of Euler angle singularities, and independence from symmetry assumptions with regard to the aircraft's moments of inertia. The model also accounts for nonlinear air density variations with altitude, up to 20 km above mean sea level, making it suitable for accurate and efficient flight dynamics simulations.

2024-12-23T05:03:13Z 22 pages, 9 figures, 3 tables, published journal article, open access, peer-reviewed International Journal of Advanced and Applied Sciences. 12(1), 30-51 (2025) Osama A. Marzouk 10.21833/ijaas.2025.01.004 http://arxiv.org/abs/2411.00031v2 2024-12-23T02:57:14Z

Solving algebra problems (APs) continues to attract significant research interest as evidenced by the large number of algorithms and theories proposed over the past decade. Despite these important research contributions, however, the body of work remains incomplete in terms of theoretical justification and scope. The current contribution intends to fill the gap by developing a review framework that aims to lay a theoretical base, create an evaluation scheme, and extend the scope of the investigation. This paper first develops the State Transform Theory (STT), which emphasizes that the problem-solving algorithms are structured according to states and transforms unlike the understanding that underlies traditional surveys which merely emphasize the progress of transforms. The STT, thus, lays the theoretical basis for a new framework for reviewing algorithms. This new construct accommodates the relation-centric algorithms for solving both word and diagrammatic algebra problems. The latter not only highlights the necessity of introducing new states but also allows revelation of contributions of individual algorithms obscured in prior reviews without this approach.

2024-10-29T08:16:49Z 22pages,5figures Xinguo Yu Weina Cheng Chuanzhi Yang Ting Zhang http://arxiv.org/abs/2412.15829v1 2024-12-20T12:12:25Z

Large knowledge graphs capture information of a large number of entities and their relations. Among the many relations they capture, class subsumption assertions are usually present and expressed using the \texttt{rdfs:subClassOf} construct. From our examination, publicly available knowledge graphs contain many potentially erroneous cyclic subclass relations, a problem that can be exacerbated when different knowledge graphs are integrated as Linked Open Data. In this paper, we present an automatic approach for resolving such cycles at scale using automated reasoning by encoding the problem of cycle-resolving to a MAXSAT solver. The approach is tested on the LOD-a-lot dataset, and compared against a semi-automatic version of our algorithm. We show how the number of removed triples is a trade-off against the efficiency of the algorithm.

2024-12-20T12:12:25Z The paper has been presented at the 2020 workshop on Large Scale RDF Analytics (LASCAR), a workshop co-located with the Extended Semantic Web Conference (ESWC) Shuai Wang Peter Bloem Joe Raad Frank van Harmelen http://arxiv.org/abs/2412.15121v1 2024-12-19T18:01:35Z

We analyze the problem of folding one polyhedron, viewed as a metric graph of its edges, into the shape of another, similar to 1D origami. We find such foldings between all pairs of Platonic solids and prove corresponding lower bounds, establishing the optimal scale factor when restricted to integers. Further, we establish that our folding problem is also NP-hard, even if the source graph is a tree. It turns out that the problem is hard to approximate, as we obtain NP-hardness even for determining the existence of a scale factor 1.5-ε. Finally, we prove that, in general, the optimal scale factor has to be rational. This insight then immediately results in NP membership. In turn, verifying whether a given scale factor is indeed the smallest possible, requires two independent calls to an NP oracle, rendering the problem DP-complete.

2024-12-19T18:01:35Z Lily Chung Erik D. Demaine Martin L. Demaine Markus Hecher Rebecca Lin Jayson Lynch Chie Nara http://arxiv.org/abs/2412.14814v1 2024-12-19T13:09:06Z

Although Answer Set Programming (ASP) allows constraining neural-symbolic (NeSy) systems, its employment is hindered by the prohibitive costs of computing stable models and the CPU-bound nature of state-of-the-art solvers. To this end, we propose Answer Set Networks (ASN), a NeSy solver. Based on Graph Neural Networks (GNN), ASNs are a scalable approach to ASP-based Deep Probabilistic Logic Programming (DPPL). Specifically, we show how to translate ASPs into ASNs and demonstrate how ASNs can efficiently solve the encoded problem by leveraging GPU's batching and parallelization capabilities. Our experimental evaluations demonstrate that ASNs outperform state-of-the-art CPU-bound NeSy systems on multiple tasks. Simultaneously, we make the following two contributions based on the strengths of ASNs. Namely, we are the first to show the finetuning of Large Language Models (LLM) with DPPLs, employing ASNs to guide the training with logic. Further, we show the "constitutional navigation" of drones, i.e., encoding public aviation laws in an ASN for routing Unmanned Aerial Vehicles in uncertain environments.

2024-12-19T13:09:06Z 16 pages, 9 figures Arseny Skryagin Daniel Ochs Phillip Deibert Simon Kohaut Devendra Singh Dhami Kristian Kersting http://arxiv.org/abs/2412.13306v1 2024-12-17T20:18:03Z

Invariants withstand transformations and, therefore, represent the essence of objects or phenomena. In mathematics, transformations often constitute a group action. Since the 19th century, studying the structure of various types of invariants and designing methods and algorithms to compute them remains an active area of ongoing research with an abundance of applications. In this incredibly vast topic, we focus on two particular themes displaying a fruitful interplay between the differential and algebraic invariant theories. First, we show how an algebraic adaptation of the moving frame method from differential geometry leads to a practical algorithm for computing a generating set of rational invariants. Then we discuss the notion of differential invariant signature, its role in solving equivalence problems in geometry and algebra, and some successes and challenges in designing algorithms based on this notion.

2024-12-17T20:18:03Z This is a tutorial paper that appeared in the proceedings of International Symposium on Symbolic and Algebraic Computation 2023 (ISSAC 2023), July 24-27, 2023, Tromsø, Norway. ACM, New York, NY, USA, https://doi.org/10.1145/3597066.3597149 . This is the author's version of the work. It is posted here for your personal use. Not for redistribution ISSAC '23: Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, Pages 31 - 40 Irina A. Kogan 10.1145/3597066.3597149 http://arxiv.org/abs/2412.08576v1 2024-12-11T17:47:49Z

Deciding the positivity of a sequence defined by a linear recurrence with polynomial coefficients and initial condition is difficult in general. Even in the case of recurrences with constant coefficients, it is known to be decidable only for order up to~5. We consider a large class of linear recurrences of arbitrary order, with polynomial coefficients, for which an algorithm decides positivity for initial conditions outside of a hyperplane. The underlying algorithm constructs a cone, contracted by the recurrence operator, that allows a proof of positivity by induction. The existence and construction of such cones relies on the extension of the classical Perron-Frobenius theory to matrices leaving a cone invariant.

2024-12-11T17:47:49Z 26 pages Alaa Ibrahim Bruno Salvy http://arxiv.org/abs/2412.08235v1 2024-12-11T09:32:11Z

Process algebras have been widely used to verify security protocols in a formal manner. However they mostly focus on synchronous communication based on the exchange of messages. We present an alternative approach relying on asynchronous communication obtained through information available on a shared space. More precisely this paper first proposes an embedding in Scala of a Linda-like language, called Bach. It consists of a Domain Specific Language, internal to Scala, that allows us to experiment programs developed in Bach while benefiting from the Scala eco-system, in particular from its type system as well as program fragments developed in Scala. Moreover, we introduce a logic that allows to restrict the executions of programs to those meeting logic formulae. Our work is illustrated on the Needham-Schroeder security protocol, for which we manage to automatically rediscover the man-in-the-middle attack first put in evidence by G. Lowe.

2024-12-11T09:32:11Z In Proceedings ICE 2024, arXiv:2412.07570 EPTCS 414, 2024, pp. 58-76 Doha Ouardi University of Namur Manel Barkallah University of Namur Jean-Marie Jacquet University of Namur 10.4204/EPTCS.414.4 http://arxiv.org/abs/2409.09359v3 2024-12-10T16:24:48Z

We present a novel method for symbolic regression (SR), the task of searching for compact programmatic hypotheses that best explain a dataset. The problem is commonly solved using genetic algorithms; we show that we can enhance such methods by inducing a library of abstract textual concepts. Our algorithm, called LaSR, uses zero-shot queries to a large language model (LLM) to discover and evolve concepts occurring in known high-performing hypotheses. We discover new hypotheses using a mix of standard evolutionary steps and LLM-guided steps (obtained through zero-shot LLM queries) conditioned on discovered concepts. Once discovered, hypotheses are used in a new round of concept abstraction and evolution. We validate LaSR on the Feynman equations, a popular SR benchmark, as well as a set of synthetic tasks. On these benchmarks, LaSR substantially outperforms a variety of state-of-the-art SR approaches based on deep learning and evolutionary algorithms. Moreover, we show that LaSR can be used to discover a novel and powerful scaling law for LLMs.

2024-09-14T08:17:30Z NeurIPS version; 10 pages; no checklist; added more experiment details Arya Grayeli Atharva Sehgal Omar Costilla-Reyes Miles Cranmer Swarat Chaudhuri http://arxiv.org/abs/2412.05586v1 2024-12-07T08:45:39Z

This work compares large language models (LLMs) and neuro-symbolic approaches in solving Raven's progressive matrices (RPM), a visual abstract reasoning test that involves the understanding of mathematical rules such as progression or arithmetic addition. Providing the visual attributes directly as textual prompts, which assumes an oracle visual perception module, allows us to measure the model's abstract reasoning capability in isolation. Despite providing such compositionally structured representations from the oracle visual perception and advanced prompting techniques, both GPT-4 and Llama-3 70B cannot achieve perfect accuracy on the center constellation of the I-RAVEN dataset. Our analysis reveals that the root cause lies in the LLM's weakness in understanding and executing arithmetic rules. As a potential remedy, we analyze the Abductive Rule Learner with Context-awareness (ARLC), a neuro-symbolic approach that learns to reason with vector-symbolic architectures (VSAs). Here, concepts are represented with distributed vectors s.t. dot products between encoded vectors define a similarity kernel, and simple element-wise operations on the vectors perform addition/subtraction on the encoded values. We find that ARLC achieves almost perfect accuracy on the center constellation of I-RAVEN, demonstrating a high fidelity in arithmetic rules. To stress the length generalization capabilities of the models, we extend the RPM tests to larger matrices (3x10 instead of typical 3x3) and larger dynamic ranges of the attribute values (from 10 up to 1000). We find that the LLM's accuracy of solving arithmetic rules drops to sub-10%, especially as the dynamic range expands, while ARLC can maintain a high accuracy due to emulating symbolic computations on top of properly distributed representations. Our code is available at https://github.com/IBM/raven-large-language-models.

2024-12-07T08:45:39Z Michael Hersche Giacomo Camposampiero Roger Wattenhofer Abu Sebastian Abbas Rahimi http://arxiv.org/abs/2412.04928v1 2024-12-06T10:32:37Z

Many articles have recently been devoted to Mahler equations, partly because of their links with other branches of mathematics such as automata theory. Hahn series (a generalization of the Puiseux series allowing arbitrary exponents of the indeterminate as long as the set that supports them is well-ordered) play a central role in the theory of Mahler equations. In this paper, we address the following fundamental question: is there an algorithm to calculate the Hahn series solutions of a given linear Mahler equation? What makes this question interesting is the fact that the Hahn series appearing in this context can have complicated supports with infinitely many accumulation points. Our (positive) answer to the above question involves among other things the construction of a computable well-ordered receptacle for the supports of the potential Hahn series solutions.

2024-12-06T10:32:37Z Journal of the London Mathematical Society, 2024, 110 (1) C. Faverjon ICJ, CTN Julien Roques ICJ, CTN 10.1112/jlms.12945