Kikuchi, Kentaro; Aoto, Takahito Confluence and commutation for nominal rewriting systems with atom-variables. (English) Zbl 07496641 Fernández, Maribel (ed.), Logic-based program synthesis and transformation. 30th international symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12561, 56-73 (2021). MSC: 68N30 PDFBibTeX XMLCite \textit{K. Kikuchi} and \textit{T. Aoto}, Lect. Notes Comput. Sci. 12561, 56--73 (2021; Zbl 07496641) Full Text: DOI
de Lima, Thaynara Arielly; Galdino, André Luiz; Avelar, Andréia Borges; Ayala-Rincón, Mauricio Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem. (English) Zbl 1493.68389 J. Autom. Reasoning 65, No. 8, 1231-1263 (2021). Reviewer: Filippo Nuccio (Saint-Étienne) MSC: 68V20 03B35 13P99 16Z05 20N02 68V15 PDFBibTeX XMLCite \textit{T. A. de Lima} et al., J. Autom. Reasoning 65, No. 8, 1231--1263 (2021; Zbl 1493.68389) Full Text: DOI
Bhayat, Ahmed; Reger, Giles Restricted combinatory unification. (English) Zbl 07178970 Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 74-93 (2019). MSC: 03B35 68V15 PDFBibTeX XMLCite \textit{A. Bhayat} and \textit{G. Reger}, Lect. Notes Comput. Sci. 11716, 74--93 (2019; Zbl 07178970) Full Text: DOI Link
Rocha-Oliveira, Ana Cristina; Galdino, André Luiz; Ayala-Rincón, Mauricio Confluence of orthogonal term rewriting systems in the prototype verification system. (English) Zbl 1407.68441 J. Autom. Reasoning 58, No. 2, 231-251 (2017). MSC: 68T15 68N30 68Q42 PDFBibTeX XMLCite \textit{A. C. Rocha-Oliveira} et al., J. Autom. Reasoning 58, No. 2, 231--251 (2017; Zbl 1407.68441) Full Text: DOI
Ayala-Rincón, Mauricio; Fernández, Maribel; Rocha-Oliveira, Ana Cristina Completeness in PVS of a nominal unification algorithm. (English) Zbl 1394.68348 Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 57-74 (2016). MSC: 68T15 03B35 68Q42 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Electron. Notes Theor. Comput. Sci. 323, 57--74 (2016; Zbl 1394.68348) Full Text: DOI
de Moura, Flávio L. C. Unification for \(\lambda\)-calculi without propagation rules. (English) Zbl 1482.68080 Sampaio, Augusto (ed.) et al., Theoretical aspects of computing – ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24–31, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9965, 179-195 (2016). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{F. L. C. de Moura}, Lect. Notes Comput. Sci. 9965, 179--195 (2016; Zbl 1482.68080) Full Text: DOI
de Moura, Flávio L. C.; Barbosa, A. V.; Ayala-Rincón, M.; Kamareddine, F. A flexible framework for visualisation of computational properties of general explicit substitutions calculi. (English) Zbl 1347.68058 Haeusler, Edward Hermann (ed.) et al., Proceedings of the 5th workshop on logical and semantic frameworks, with applications (LSFA 2010), Natal, Brazil, August 31, 2010. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 269, 41-54 (2011). MSC: 68N18 68Q42 PDFBibTeX XMLCite \textit{F. L. C. de Moura} et al., Electron. Notes Theor. Comput. Sci. 269, 41--54 (2011; Zbl 1347.68058) Full Text: DOI
de Moura, Flávio L. C.; Ayala-Rincón, Mauricio; Kamareddine, Fairouz Higher-order unification: a structural relation between Huet’s method and the one based on explicit substitutions. (English) Zbl 1138.03014 J. Appl. Log. 6, No. 1, 72-108 (2008). MSC: 03B40 03B25 03B35 PDFBibTeX XMLCite \textit{F. L. C. de Moura} et al., J. Appl. Log. 6, No. 1, 72--108 (2008; Zbl 1138.03014) Full Text: DOI
de Moura, F. L. C.; Ayala-Rincón, M.; Kamareddine, F. SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi. (English) Zbl 1184.68469 J. Appl. Non-Class. Log. 16, No. 1-2, 119-150 (2006). MSC: 68T15 03B40 PDFBibTeX XMLCite \textit{F. L. C. de Moura} et al., J. Appl. Non-Class. Log. 16, No. 1--2, 119--150 (2006; Zbl 1184.68469) Full Text: DOI