Zobrazeno 1 - 7
of 7
pro vyhledávání: '"Andréia B. Avelar"'
Autor:
Muñoz, Cesar A., Ayala-Rincón, Mauricio, Moscato, Mariano M., Dutle, Aaron M., Narkawicz, Anthony J., Almeida, Ariane Alves, da Silva, Andréia B. Avelar, Ramos, Thiago M. Ferreira
Publikováno v:
Journal of Automated Reasoning; Dec2023, Vol. 67 Issue 4, p1-30, 30p
Publikováno v:
Journal of Automated Reasoning. 65:1231-1263
This paper presents a PVS development of relevant results of the theory of rings. The PVS theory includes complete proofs of the three classical isomorphism theorems for rings, and characterizations of principal, prime and maximal ideals. Algebraic c
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::aefafd3f76ad0539d92a776066ac7b88
https://doi.org/10.1007/s10817-021-09593-0
https://doi.org/10.1007/s10817-021-09593-0
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 81, Iss Proc. LSFA 2011, Pp 63-78 (2012)
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 feature of this formalization is that it remains close to the textbook proof
Externí odkaz:
https://doaj.org/article/d2ce367afa5846a39a22e7c4e7c54628
Publikováno v:
Interactive Theorem Proving ISBN: 9783319948201
ITP
ITP
This work describes the ongoing specification and formalization in the PVS proof assistant of some definitions and theorems of ring theory in abstract algebra, and briefly presents some of the results intended to be formalized. So far, some important
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5ec6402b937b8ed4187086e7b5aaf8a5
https://doi.org/10.1007/978-3-319-94821-8_3
https://doi.org/10.1007/978-3-319-94821-8_3
Autor:
Flávio Leonardo Cavalcanti de Moura, André Luiz Galdino, Andréia B. Avelar, Mauricio Ayala-Rincón
Publikováno v:
Logic Journal of IGPL. 22:758-789
This work presents formalizations of properties and algorithms for the first-order unification theory in the proof assistant PVS. In previous works a formalization of the theorem of existence of most general unifiers (mgu's) for first-order unifiable
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::babd51c2a6f159a9a12145332e45ed44
https://doi.org/10.1093/jigpal/jzu012
https://doi.org/10.1093/jigpal/jzu012
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 81, Iss Proc. LSFA 2011, Pp 63-78 (2012)
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 feature of this formalization is that it remains close to the textbook proof
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c9eeb0aa40e84167c8f176dbf5ed58fa
http://arxiv.org/abs/1203.6160
http://arxiv.org/abs/1203.6160
Publikováno v:
Logic, Language, Information and Computation ISBN: 9783642138232
WoLLIC
WoLLIC
This work presents a general methodology for verification of the completeness of first-order unification algorithms a la Robinson developed in the higher-order proof assistant PVS. The methodology is based on a previously developed formalization of t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bceb996296619b6cf17b3e91d922b4db
https://doi.org/10.1007/978-3-642-13824-9_10
https://doi.org/10.1007/978-3-642-13824-9_10