This document briefly discusses the current development status of the computational algebra library DoCon-A using the Agda language. Strictly speaking, Agda is an extension of the Haskell language with dependent types. In such a system, computing programs are accompanied by formal proofs of their most important properties (chosen by the programmer), and these proofs are automatically verified by the system. The next challenge is to construct a constructive proof program for the most general method of computing the GCD of multivariate polynomials. By default (in Agda), preference is given to constructive logic. However, in certain cases, it becomes necessary to use a suitable special case of the Law of Excluded Middle. The general method for GCD of polynomials turned out to be the first instance of violating the purity of constructivism in this project.
S. D. MESHVELIANI (Wed,) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: