Ayala-Rincón, Mauricio; Fernández, Maribel; Silva, Gabriel Ferreira; Kutsia, Temur; Nantes-Sobrinho, Daniele Nominal AC-matching. (English) Zbl 07810723 Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 53-68 (2023). MSC: 68Vxx PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Lect. Notes Comput. Sci. 14101, 53--68 (2023; Zbl 07810723) Full Text: DOI
Ayala-Rincón, Mauricio; De Carvalho-Segundo, Washington; Fernández, Maribel; Silva, Gabriel Ferreira; Nantes-Sobrinho, Daniele Formalising nominal C-unification generalised with protected variables. (English) Zbl 1495.68109 Math. Struct. Comput. Sci. 31, No. 3, 286-311 (2021). MSC: 68Q42 68V20 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Math. Struct. Comput. Sci. 31, No. 3, 286--311 (2021; Zbl 1495.68109) Full Text: DOI
Ayala-Rincón, Mauricio; Fernández, Maribel; Silva, Gabriel Ferreira; Nantes-Sobrinho, Daniele A certified functional nominal C-unification algorithm. (English) Zbl 1502.68145 Gabbrielli, Maurizio (ed.), Logic-based program synthesis and transformation. 29th international symposium, LOPSTR 2019, Porto, Portugal, October 8–10, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12042, 123-138 (2020). MSC: 68Q42 68Q60 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Lect. Notes Comput. Sci. 12042, 123--138 (2020; Zbl 1502.68145) Full Text: DOI
Ayala-Rincón, Mauricio; Fernández, Maribel; Sobrinho, Daniele Nantes; Vale, Deivid On solving nominal disunification constraints. (English) Zbl 1495.03048 Felty, Amy (ed.) et al., 14th international workshop on logical and semantic frameworks, with applications, LSFA 2019, Natal, Brazil, in August 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 348, 3-22 (2020). MSC: 03B70 03B40 68Q55 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Electron. Notes Theor. Comput. Sci. 348, 3--22 (2020; Zbl 1495.03048) Full Text: DOI
Ayala-Rincón, Mauricio; Fernández, Maribel; Nantes-Sobrinho, Daniele On nominal syntax and permutation fixed points. (English) Zbl 1528.68152 Log. Methods Comput. Sci. 16, No. 1, Paper No. 19, 36 p. (2020). MSC: 68Q42 68N30 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Log. Methods Comput. Sci. 16, No. 1, Paper No. 19, 36 p. (2020; Zbl 1528.68152) Full Text: arXiv
Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele A formalisation of nominal C-matching through unification with protected variables. (English) Zbl 1433.68186 Accattoli, Beniamino (ed.) et al., Proceedings of the 13th workshop on logical and semantic frameworks with applications, LSFA 18, Fortaleza, Brazil, September 26–28, 2018. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 344, 47-65 (2019). MSC: 68Q42 68V15 68V20 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Electron. Notes Theor. Comput. Sci. 344, 47--65 (2019; Zbl 1433.68186) Full Text: DOI
Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele; Rocha-Oliveira, Ana Cristina A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols. (English) Zbl 1423.68405 Theor. Comput. Sci. 781, 3-23 (2019). MSC: 68T15 03B70 68Q25 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Theor. Comput. Sci. 781, 3--23 (2019; Zbl 1423.68405) Full Text: DOI Link
Ayala-Rincón, Mauricio; Fernández, Maribel; Nantes-Sobrinho, Daniele Fixed-point constraints for nominal equational unification. (English) Zbl 1462.68089 Kirchner, Hélène (ed.), 3rd international conference on formal structures for computation and deduction, FSCD 2018, July 9–12, 2018, Oxford, United Kingdom. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 108, Article 7, 16 p. (2018). MSC: 68Q42 03B70 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., LIPIcs -- Leibniz Int. Proc. Inform. 108, Article 7, 16 p. (2018; Zbl 1462.68089) Full Text: DOI
Ayala-Rincón, Mauricio; de Carvalho-Segundo, Washington; Fernández, Maribel; Nantes-Sobrinho, Daniele A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols. (English) Zbl 1401.68273 Nigam, Vivek (ed.) et al., Proceedings of the 11th workshop on logical and semantic frameworks, with applications (LSFA 2016), Porto, Portugal, 2016. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 332, 21-38 (2017). MSC: 68T15 03B70 68Q25 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Electron. Notes Theor. Comput. Sci. 332, 21--38 (2017; Zbl 1401.68273) Full Text: DOI
Copello, Ernesto; Tasistro, Álvaro; Szasz, Nora; Bove, Ana; Fernández, Maribel Alpha-structural induction and recursion for the lambda calculus in constructive type theory. (English) Zbl 1395.68085 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, 109-124 (2016). MSC: 68N18 03B15 03B40 PDFBibTeX XMLCite \textit{E. Copello} et al., Electron. Notes Theor. Comput. Sci. 323, 109--124 (2016; Zbl 1395.68085) 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
Ayala-Rincón, Mauricio; Fernández, Maribel; Gabbay, Murdoch James; Rocha-Oliveira, Ana Cristina Checking overlaps of nominal rewriting rules. (English) Zbl 1401.68131 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, 39-56 (2016). MSC: 68Q42 PDFBibTeX XMLCite \textit{M. Ayala-Rincón} et al., Electron. Notes Theor. Comput. Sci. 323, 39--56 (2016; Zbl 1401.68131) Full Text: DOI
Fernández, Maribel AC complement problems: satisfiability and negation elimination. (English) Zbl 1503.03017 Kirchner, Claude (ed.), Rewriting techniques and applications. 5th international conference RTA-93, Montréal, Canada, June 16–18, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 690, 358-373 (1993). MSC: 03B35 68Q42 PDFBibTeX XMLCite \textit{M. Fernández}, Lect. Notes Comput. Sci. 690, 358--373 (1993; Zbl 1503.03017) Full Text: DOI
Comon, Hubert; Fernández, Maribel Negation elimination in equational formulae (extended abstract). (English) Zbl 1496.03040 Havel, Ivan M. (ed.) et al., Mathematical foundations of computer science 1992. 17th international symposium, Prague, Czechoslovakia, August 24–28, 1992. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 629, 191-199 (1992). MSC: 03B35 68Q42 PDFBibTeX XMLCite \textit{H. Comon} and \textit{M. Fernández}, Lect. Notes Comput. Sci. 629, 191--199 (1992; Zbl 1496.03040) Full Text: DOI