{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:56:37Z","timestamp":1776552997493,"version":"3.51.2"},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This talk discusses current extensions on the theory algebra from the NASA\/PVSlibrary on formal developments for the Prototype Verification System (PVS). It discusses the approach to formalizing theorems of the ring theory and how they are applied to infer properties of specific algebraic structures. As cases of study, we will present recent formalizations on the theories of Euclidean Domains and Quaternions. Moreover, we will show how a general verification of Euclid\u2019s division algorithm can be specialized to verify this algorithm for specific Euclidean Domains, and how the abstract theory of Quaternions can be parameterized to deal with the structure of Hamilton\u2019s Quaternions.<\/jats:p>","DOI":"10.29007\/7jbv","type":"proceedings-article","created":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:10Z","timestamp":1685815810000},"page":"1--10","source":"Crossref","is-referenced-by-count":2,"title":["Formalization of Algebraic Theorems in PVS (Invited Talk)"],"prefix":"10.29007","volume":"94","author":[{"given":"Mauricio","family":"Ayala-Rinc\u00f3n","sequence":"first","affiliation":[]},{"given":"Thaynara","family":"Arielly de Lima","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9ia B.","family":"Avelar","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9 Luiz","family":"Galdino","sequence":"additional","affiliation":[]}],"member":"11545","event":{"name":"Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning"},"container-title":["EPiC Series in Computing"],"original-title":[],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T18:10:16Z","timestamp":1685815816000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/93F2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/7jbv","relation":{},"ISSN":["2398-7340"],"issn-type":[{"value":"2398-7340","type":"print"}],"subject":[]}}