4 citations · 11 across the 5 of their papers we have counts for
8 papers · 1 filter
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…
Equational Anti-Unification over Absorption Theories
Mauricio Ayala-Rincon, David M. Cerna, Andres Felipe Gonzalez Barragan +1
Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unifica…
Proceedings 16th Logical and Semantic Frameworks with Applications
Mauricio Ayala-Rincon, Eduardo Bonelli
This volume contains the post-proceedings of the Sixteenth Logical and Semantic Frameworks with Applications (LSFA 2021). The meeting was held online on July 23-24, 2021, organised…
Teaching Interactive Proofs to Mathematicians
Mauricio Ayala-Rincón, Thaynara Arielly de Lima
This work discusses an approach to teach to mathematicians the importance and effectiveness of the application of Interactive Theorem Proving tools in their specific fields of inte…
Formalizing the Dependency Pair Criterion for Innermost Termination
Ariane Alves Almeida, Mauricio Ayala-Rincon
Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Funct…
Formalising Confluence in PVS
Mauricio Ayala-Rincón
Confluence is a critical property of computational systems which is related with determinism and non ambiguity and thus with other relevant computational attributes of functional s…