Nº 4 (2023)

In this paper, we consider a constructive proof of the termination of the normal form (NF) algorithm for multivariate polynomials, as well as the related concept of admissible ordering < on monomials. In classical mathematics, the well-quasiorder property of relation < is derived from Dickson’s lemma, and this is sufficient to justify the termination of the NF algorithm. In provable programming based on constructive type theory (Coq and Agda), a somewhat stronger condition (in constructive mathematics) of the wellfoundedness of the ordering (in its constructive version) is required. We propose a constructive proof of this theorem (T) for < , which is based on a known method that we refer to here as the “pattern method.” This theorem on the well-foundedness of an arbitrary admissible ordering is also important in itself, independently of the NF algorithm. We are not aware of any other works on constructive proof of this theorem. However, it turns out that it follows, not very difficultly, from the results achieved by other researchers in 2003. We program this proof in the Agda language in the form of our library AdmissiblePPO-wellFounded of provable computational algebra programs. This development also uses the theorem to prove termination of the NF algorithm for polynomials. Thus, the library also contains a set of provable programs for polynomial algebra, which is significantly larger than that needed to prove Theorem T.

Methods of computer algebra are used to investigate equilibrium orientations of a satellite moving along a circular orbit under the action of gravitational and constant torques. The main focus is placed on the investigation of equilibrium orientations in the cases where the constant torque vector is parallel to the planes formed by the principal central axes of inertia of the satellite. Using methods for Gröbner basis construction, the system of six algebraic equations that determine the equilibrium orientations of the satellite is reduced to one sixth-order algebraic equation in one unknown. Domains with equal numbers of equilibrium solutions are classified using algebraic methods for constructing discriminant hypersurfaces. Bifurcation curves in the space of problem parameters, which define the boundaries of the domains with equal numbers of equilibrium solutions, are constructed. A comparative analysis of the influence of the order of variables in the process of Gröbner basis construction is carried out. Using the proposed approach, it is shown that, under the action of the constant torque, the satellite with unequal principal central moments of inertia has no more than 24 equilibrium orientations in a circular orbit.

Formal proof of security measure effectiveness and computation security is vitally important for trust in critical information systems. It should be realized that formal security verification must be carried out at each infrastructural level (from the hardware level to the application level) in the process of system design. Currently, computation security analysis on the application level remains the major challenge as it requires complex labeling of computing environment elements. Traditionally, to solve this problem, information flow control (IFC) methods are employed. Unlike access control mechanisms widely used in modern operating systems (OSs) and database management systems (DBMSs), IFC has limited application in software design and mostly comes down to trivial taint tracking. This paper describes an approach to full-fledged implementation of IFC in PL/SQL program units with the use of the PLIF platform. In addition, a general scheme of computation security analysis for enterprise applications that work with relational DBMSs is considered. The key advantage of our approach is the explicit separation of functions between software developers and security analysts.

A new version of GInv (Gröbner Involutive) for computing involutive Gröbner bases is presented as a library in C++11. GInv uses object-oriented memory reallocation for dynamic data structures, such as lists, red-black trees, binary trees, and GMP libraries for arbitrary-precision integer calculations. The interface of the package is designed as a Python3 module.