most citedFormalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms

2 citations · 3 across the 2 of their papers we have counts for

collaborators
Showing cs.LOShow all

2 papers · 1 filter

cs.LO2024★ 2 cited

Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms

Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino +1

This paper discusses the extension of the Prototype Verification System (PVS) sub-theory for rings, part of the PVS algebra theory, with theorems related to the division algorithm…

cs.LO2012★ 1 cited

A Formalization of the Theorem of Existence of First-Order Most General Unifiers

Andréia B Avelar, André L Galdino, Flávio LC de Moura +1

This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing featur…