Zobrazeno 1 - 6
of 6
pro vyhledávání: '"André L. Galdino"'
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:
LSFA
A theory, called trs, for Term Rewriting Systems in the theorem Prover PVS is described. This theory is built on the PVS libraries for finite sequences and sets and a previously developed PVS theory named ars for Abstract Reduction Systems which was
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b6881bbc1bfe7017cb79a0a8d4df45aa
https://doi.org/10.1016/j.entcs.2009.07.049
https://doi.org/10.1016/j.entcs.2009.07.049
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:
CLEI Electronic Journal, Vol 11, Iss 2 (2008)
A theory for Abstract Reduction Systems (ARS) in the proof assistant PVS (Prototype Verification System) called ars is described. Adequate specifications of basic definitions and notions of the theory of ARSs such as reduction, confluence and normal
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::db537be0c9f35250f7d4934bd3941376
http://clei.org/cleiej-beta/index.php/cleiej/article/view/273
http://clei.org/cleiej-beta/index.php/cleiej/article/view/273
Publikováno v:
Logic, Language, Information and Computation ISBN: 9783540734437
WoLLIC
WoLLIC
Highly accurate positioning systems and new broadcasting technology have enabled air traffic management concepts where the responsibility for aircraft separation resides on pilots rather than on air traffic controllers. The Formal Methods Group at th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0aa13d7b71fc2be7e718f8039ec07b35
https://doi.org/10.1007/978-3-540-73445-1_13
https://doi.org/10.1007/978-3-540-73445-1_13