Search Results

Documents authored by Ayala-Rincón, Mauricio

Document
DOI: 10.4230/LIPIcs.ITP.2024.11
A Formalization of the General Theory of Quaternions

Authors: Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
This paper discusses the formalization of the theory of quaternions in the Prototype Verification System (PVS). The general approach in this mechanization relies on specifying quaternion structures using any arbitrary field as a parameter. The approach allows the inheritance of formalized properties on quaternions when the parameters of the general theory are instantiated with specific fields such as reals or rationals. The theory includes characterizing algebraic properties that lead to constructing quaternions as division rings. In particular, we illustrate how the general theory is applied to formalize Hamilton’s quaternions using the field of reals as a parameter, for which we also mechanized theorems that show the completeness of three-dimensional rotations, proving that Hamilton’s quaternions mimic any 3D rotation.
Cite as

Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón. A Formalization of the General Theory of Quaternions. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{delima_et_al:LIPIcs.ITP.2024.11,
  author =	{de Lima, Thaynara Arielly and Galdino, Andr\'{e} Luiz and de Oliveira Ribeiro, Bruno Berto and Ayala-Rinc\'{o}n, Mauricio},
  title =	{{A Formalization of the General Theory of Quaternions}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{11:1--11:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.11},
  URN =		{urn:nbn:de:0030-drops-207398},
  doi =		{10.4230/LIPIcs.ITP.2024.11},
  annote =	{Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2022.8
A Certified Algorithm for AC-Unification

Authors: Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes Sobrinho

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract
Implementing unification modulo Associativity and Commutativity (AC) axioms is crucial in rewrite-based programming and theorem provers. We modify Stickel’s seminal AC-unification algorithm to avoid mutual recursion and formalise it in the PVS proof assistant. More precisely, we prove the adjusted algorithm’s termination, soundness, and completeness. To do this, we adapted Fages' termination proof, providing a unique elaborated measure that guarantees termination of the modified AC-unification algorithm. This development (to the best of our knowledge) provides the first fully formalised AC-unification algorithm.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, and Daniele Nantes Sobrinho. A Certified Algorithm for AC-Unification. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 8:1-8:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2022.8,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Silva, Gabriel Ferreira and Sobrinho, Daniele Nantes},
  title =	{{A Certified Algorithm for AC-Unification}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{8:1--8:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.8},
  URN =		{urn:nbn:de:0030-drops-162894},
  doi =		{10.4230/LIPIcs.FSCD.2022.8},
  annote =	{Keywords: AC-Unification, PVS, Certified Algorithms, Formal Methods, Interactive Theorem Proving}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.27
Formal Verification of Termination Criteria for First-Order Recursive Functions

Authors: Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane A. Almeida, Andréia B. Avelar, and Thiago M. Ferreira Ramos

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
This paper presents a formalization of several termination criteria for first-order recursive functions. The formalization, which is developed in the Prototype Verification System (PVS), includes the specification and proof of equivalence of semantic termination, Turing termination, size change principle, calling context graphs, and matrix-weighted graphs. These termination criteria are defined on a computational model that consists of a basic functional language called PVS0, which is an embedding of recursive first-order functions. Through this embedding, the native mechanism for checking termination of recursive functions in PVS could be soundly extended with semi-automatic termination criteria such as calling contexts graphs.
Cite as

Cesar A. Muñoz, Mauricio Ayala-Rincón, Mariano M. Moscato, Aaron M. Dutle, Anthony J. Narkawicz, Ariane A. Almeida, Andréia B. Avelar, and Thiago M. Ferreira Ramos. Formal Verification of Termination Criteria for First-Order Recursive Functions. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{munoz_et_al:LIPIcs.ITP.2021.27,
  author =	{Mu\~{n}oz, Cesar A. and Ayala-Rinc\'{o}n, Mauricio and Moscato, Mariano M. and Dutle, Aaron M. and Narkawicz, Anthony J. and Almeida, Ariane A. and Avelar, Andr\'{e}ia B. and M. Ferreira Ramos, Thiago},
  title =	{{Formal Verification of Termination Criteria for First-Order Recursive Functions}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.27},
  URN =		{urn:nbn:de:0030-drops-139228},
  doi =		{10.4230/LIPIcs.ITP.2021.27},
  annote =	{Keywords: Formal Verification, Termination, Calling Context Graph, PVS}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.7
Fixed-Point Constraints for Nominal Equational Unification

Authors: Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We propose a new axiomatisation of the alpha-equivalence relation for nominal terms, based on a primitive notion of fixed-point constraint. We show that the standard freshness relation between atoms and terms can be derived from the more primitive notion of permutation fixed-point, and use this result to prove the correctness of the new alpha-equivalence axiomatisation. This gives rise to a new notion of nominal unification, where solutions for unification problems are pairs of a fixed-point context and a substitution. Although it may seem less natural than the standard notion of nominal unifier based on freshness constraints, the notion of unifier based on fixed-point constraints behaves better when equational theories are considered: for example, nominal unification remains finitary in the presence of commutativity, whereas it becomes infinitary when unifiers are expressed using freshness contexts.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2018.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Fixed-Point Constraints for Nominal Equational Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{7:1--7:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.7},
  URN =		{urn:nbn:de:0030-drops-91777},
  doi =		{10.4230/LIPIcs.FSCD.2018.7},
  annote =	{Keywords: nominal terms, fixed-point equations, nominal unification, equational theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2016.11
Nominal Narrowing

Authors: Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract
Nominal unification is a generalisation of first-order unification that takes alpha-equivalence into account. In this paper, we study nominal unification in the context of equational theories. We introduce nominal narrowing and design a general nominal E-unification procedure, which is sound and complete for a wide class of equational theories. We give examples of application.
Cite as

Mauricio Ayala-Rincón, Maribel Fernández, and Daniele Nantes-Sobrinho. Nominal Narrowing. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2016.11,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Fern\'{a}ndez, Maribel and Nantes-Sobrinho, Daniele},
  title =	{{Nominal Narrowing}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.11},
  URN =		{urn:nbn:de:0030-drops-59832},
  doi =		{10.4230/LIPIcs.FSCD.2016.11},
  annote =	{Keywords: Nominal Rewriting, Nominal Unification, Matching, Narrowing, Equational Theories}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.391
Metaconfluence of Calculi with Explicit Substitutions at a Distance

Authors: Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Confluence is a key property of rewriting calculi that guarantees uniqueness of normal-forms when they exist. Metaconfluence is even more general, and guarantees confluence on open/meta terms, i.e. terms with holes, called metavariables that can be filled up with other (open/meta) terms. The difficulty to deal with open terms comes from the fact that the structure of metaterms is only partially known, so that some reduction rules became blocked by the metavariables. In this work, we establish metaconfluence for a family of calculi with explicit substitutions (ES) that enjoy preservation of strong-normalization (PSN) and that act at a distance. For that, we first extend the notion of reduction on metaterms in such a way that explicit substitutions are never structurally moved, i.e. they also act at a distance on metaterms. The resulting reduction relations are still rewriting systems, i.e. they do not include equational axioms, thus providing for the first time an interesting family of lambda-calculi with explicit substitutions that enjoy both PSN and metaconfluence without requiring sophisticated notions of reduction modulo a set of equations.
Cite as

Flávio L. C. de Moura, Delia Kesner, and Mauricio Ayala-Rincón. Metaconfluence of Calculi with Explicit Substitutions at a Distance. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 391-402, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{demoura_et_al:LIPIcs.FSTTCS.2014.391,
  author =	{de Moura, Fl\'{a}vio L. C. and Kesner, Delia and Ayala-Rinc\'{o}n, Mauricio},
  title =	{{Metaconfluence of Calculi with Explicit Substitutions at a  Distance}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{391--402},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.391},
  URN =		{urn:nbn:de:0030-drops-48588},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.391},
  annote =	{Keywords: Confluence, Explicit Substitutions, Lambda Calculi}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact