2 citations · 3 across the 2 of their papers we have counts for
2 papers
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…