Reports and Publications M. Ayala-Rincón

See also: MathSciNet DBLP Orcid IEEE ACM Scopus Math. Genealogy

Work in progress

  • M. Ayala-Rincón et al. Nominal Equational Reasoning IT presented at LSFA 2020. Slides.
  • T.A. de Lima and M. Ayala-Rincón NP-Completeness of Sorting Unsigned Permutations by Reversals . Note MAT/UnB pdf, Brasília, 2013.
  • M. Ayala-Rincón, Besik Dundua, Temur Kutsia and Mircea Marin Rewriting Logic from a rhoLog Point of View, Presented at LSFA 2017.
  • T.M. Ferreira Ramos, A.A. Almeida, and M. Ayala-Rincón Formalization of the Computational Theory of a Turing Complete Functional Language Model. (pdf file, PVS theory), submitted 2020.
  • L. A. da Silveira, J. L. Soncco-Álvarez, J. de Barros, C. H. Llanos, and M. Ayala-Rincón On The Behaviour of Parallel Island Models, Submitted. See extended version at genoma site
  • M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández, G.F. Silva, and D. Nantes-Sobrinho, Formalising Nominal C-Matching through Unification with Protected Variables. Submitted extended version (pdf) of paper presented at LSFA 2018, 2020.
  • T. A. de Lima, A. L. Galdino, A. Borges Avelar, and M. Ayala-Rincón, Formalization of Ring Theory in PVS - Isomorphism Theorems, Principal, Prime and Maximal Ideals,Chinese Remainder Theorem. Source: PVS 6 files, PVS 7.0 files (snapshot 1218 Allegro), (pdf). Submitted 2020.
  • M. Ayala-Rincón and T. A. de Lima, Teaching Interactive Proofs to Mathematicians. PVS 7.0 source, To appear in post-proceedings 9th International Workshop on Theorem Prover Components for Educational Software (ThEdu), 2020.
  • M. Ayala-Rincón and G.F. Silva, Why We Need Structured Proofs in Mathematics. Submitted extended abstrct (pdf), Presentation in Workshop on Natural Formal Mathematics (affiliated to CICM-13), NFM, 2020.

Editorial work: Proceedings and Special Issues

  • Mauricio Ayala-Rincón, and Samuel Mimram: Proceedings of the Ninth International Workshop on Confluence IWC 2020 (with system descriptions from CoCo 2020), pdf, 2020.
  • Mauricio Ayala-Rincón, Silvia Ghilezan, and Jakob Grue Simonsen: Joint Proceedings of HOR 2019 and IWC 2019 (with system descriptions from CoCo 2019), pdf, 2019.
  • Mauricio Ayala-Rincón, and César A. Muñoz: Special Issue of selected extended papers of the Eighth International Conference on Interactive Theorem Proving. Journal of Automated Reasoning vol. 63(2), 2019, Contents
  • Mauricio Ayala-Rincón, César A. Muñoz: Proc. 8th International Conference on Interactive Theorem Proving (ITP 2017). Springer LNCS vol. 10499, 2017
  • Mauricio Ayala-Rincón, Ian Mackie and Ugo Montanari: Special Issue of Logical and Semantic Frameworks with Applications (LSFA 2014). Theor. Comput. Sci. vol. 685, 2017. Contents
  • Mauricio Ayala-Rincón, Ian Mackie: Proceeding 9th Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2014). Electr. Notes Theor. Comput. Sci. vol. 312, 2015. Contents
  • Mauricio Ayala-Rincón, Eduardo Bonelli, Ian Mackie: Proc. 9th International Workshop on Developments in Computational Models (DCM 2013). EPTCS vol. 144, 2014. Contents
  • Mauricio Ayala-Rincón, Elaine Pimentel, Fairouz Kamareddine: Special Issue of Logical and Semantic Frameworks with Applications (LSFA 2008 and 2009). Theor. Comput. Sci. vol. 412(37), 2011. Contents
  • Mauricio Ayala-Rincón, Fairouz Kamareddine: Proc. of the Fourth Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2009). Electr. Notes Theor. Comput. Sci. vol. 256, 2009. Contents
  • Mauricio Ayala-Rincón, Edward Hermann Haeusler: Special Issue of Logical and Semantic Frameworks, with Applications (LSFA 2007). Logic Journal of the IGPL vol. 17(5): 487-488, 2009. Contents
  • Mauricio Ayala-Rincón, Edward Hermann Haeusler: Proc. of the Second Workshop on Logical and Semantic Frameworks, with Applications (LSFA 2007). Electr. Notes Theor. Comput. Sci. vol. 205, 2008. Contents

Books



M. Ayala-Rincón & Flávio L.C. de Moura, Applied Logic for Computer Scientists: Computational Deduction and Formal Proofs, Springer, 2017.





M. Ayala-Rincón & Flávio L.C. de Moura, Fundamentos da Programação Lógica e Funcional - O Princípio de Resolução e a Teoria de Reescrita -, Course Notes, Ed. UnB, December 2014. In Portuguese.

Tutorials

Publications by year

2020

  • L. A. da Silveira, J. L. Soncco-Álvarez, T. A. de Lima, and M. Ayala-Rincón Behaviour of Bioinspired Algorithms in Parallel Island Models See extended version at genoma site. 2020 IEEE Congress on Evolutionary Computation CeC 2020, (doi).
  • A.A. Almeida, and M. Ayala-Rincón Formalizing the Dependency Pairs Criterion for Innermost Termination. Associated formalization available as part of the PVS term rewriting systems theory at trs). Version presented at SBMF 2019 ArXiv. Journal version in Science of Computer Programming (Online doi), 2020.
  • M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho On Nominal Syntax and Permutation Fixed Points. Logical Methods in Computer Science 16(1):19:1-36, 2020 (arXiv / pdf LMCS / doi)
  • M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho and D. Vale On Solving Nominal Disunification Constraints, Revised papers Proc. LSFA 2019, ENTCS Vol. 348:Pages 3-22, 2020 (doi).
  • M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho and D. Vale. An Investigation into General Nominal Equational Problems, Proc. 34th International Workshop on Unification (UNIF), Temur Kutsia and Andrew M. Marshall (Eds.), RISC-Linz Report Series No. 20-10, pp.3:1-8, 2020.
  • J. Barreto, C.H. Llanos, and M. Ayala-Rincón Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wromhole-based Real-time Network-on-chip , 2019 IX Brazilian Symposium on ..., IEEE Xplore 2020 (doi).
  • M. Ayala-Rincón, M. Fernández, G. Ferreira Silva and D. Nantes-Sobrinho A Certified Functional Nominal C-Unification Algorithm. In Post-proceddings Logic-Based Program Synthesis and Transformation (LoPSTR 2019), Springer, LNCS vol. 12042:1-16, (PVS formalisation in site Nominal), (doi), 2020.

2019

  • M. Ayala-Rincón, M. Fernández, G. Ferreira Silva and D. Nantes-Sobrinho A Certified Functional Nominal C-Unification Algorithm. Presented at LOPSTR 2019 (LOPSTR Informal pre-proceedings ). Extended version: (pdf).
  • A.A. Almeida, A.C. Rocha-Oliveira, T.M.F. Ramos, F.L.C. de Moura, and M. Ayala-Rincón The Computational Relevance of Formal Logic Through Formal Proofs. In FMTea 2019, Proc. FMTea, Springer LNCS vol. 11758:81-96, 2019 (doi).
  • L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Parallel Island models Genetic Algorithms applied in NP-Hard problems (pdf at genoma project page). 2019 IEEE Congress on Evolutionary Computation CeC 2019, (doi).
  • M. Ayala-Rincón, M. Fernández and G. Ferreira Silva Formalising Nominal AC-Unification. Presented at UNIF 2019.
  • M. Ayala-Rincón, E. Bonelli, J. Edi and A. Viso Typed Path Polymorphism, Theoretical Computer Science Vol. 781:111-130 (doi), 2019.
  • M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho, and A.C. Rocha-Oliveira A Formalisation of Nominal alpha-equivalence with A, C, and AC Function Symbols. (Coq formalisation, PDF), Theoretical Computer Science Vol. 781:3-23 (doi), 2019.
  • J.L. Soncco-Álvarez, D.M. Muñoz and M. Ayala-Rincón Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals, Evolutionary Computation Vol. 27(2):229-265 (doi), 2019.

2018

2017

  • M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho Nominal C-Unification, Pre-Proceedings ArXiv version presented at LOPSTR, 2017.
  • M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho On solving nominal fixpoint equations - pdf, In Proc. 11th International Symposium on Frontiers of Combining Systems - FroCoS, Springer Nature LNAI vol. 10483:209-226, (doi), 2017.
  • L.A. da Silveira, J.L. Soncco-Álvarez and M. Ayala-Rincón Parallel Genetic Algorithms with Sharing of Individuals for Sorting Unsigned Genomes by Reversals. 2017 IEEE Congress on Evolutionary Computation (CEC), 741-748 (doi), 2017.
  • J.L. Soncco-Álvarez and M. Ayala-Rincón Variable Neighborhood Search for the Large Phylogeny Problem using Gene Order Data. Presented at 2017 IEEE Congress on Evolutionary Computation (CEC), pp 59-66 (doi), 2017.
  • M. Ayala-Rincón, W. de Carvalho-Segundo, M. Fernández and D. Nantes-Sobrinho A Formalisation of Nominal alpha-equivalence with A and AC Function Symbols ENTCS 332:21-38 (doi), 2017.
  • M. Ayala-Rincón, M. Fernández and D. Nantes-Sobrinho Intruder Deduction Problem for Locally Stable Theories with Normal Forms and Inverses. Theoretical Computer Science 672:64-100 (doi), 2017.
  • A.C. Rocha-Oliveira, A.L. Galdino and M. Ayala-Rincón Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System. Journal of Automated Reasoning 58(2):231-251 (doi), 2017.

2016

2015

  • M. Ayala-Rincón, Invited Talk Formalising Confluence given in the 11th Developments in Computational Models - DCM 2015 (satellite of the 12th Int. Coll. on Theoretical Aspects of Computing ICTAC 2015), Cali, Colombia, 28 October 2015.
  • L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations. PDF, C code, Proc. NaBIC 2015 (Vol.419, series Advances in Intelligent Systems and Computing pp 73-85, 2016). (doi).
  • L.A. da Silveira, J.L. Soncco-Álvarez, T.A. de Lima and M. Ayala-Rincón Computing Translocation Distance by a Genetic Algorithm. PDF, C code, IEEE Xplore Proceedings CLEI 2015. (doi).
  • M. Ayala-Rincón, Tutorial on Formal Reasoning with PVS given in the Nat@logic Reasoning School 2015, Natal, Brazil, 31 August - 1 September 2015.
  • A. Viso, E. Bonelli and M. Ayala-Rincón, Type Soundness for Path Polymorphism. Pre-proceedings LSFA 2015:3-18, 2015, ArXiv extended version. ENTCS 2016 (doi).
  • M. Ayala-Rincón, M. Fernández and A.C. Rocha-Oliveira, Completeness in PVS of a Nominal Unification Algorithm. Pre-proceedings LSFA 2015:19-34, 2015. ENTCS 2016 (doi).
  • A.C. Rocha-Oliveira, M. Ayala-Rincón and M. Fernández Formalising the Completeness of a Nominal Unification Algorithm. Ext. abstract presented in UNIF 2015 (RDP). Inf. Proc. 29th Int. Workshop on Unification, pp:27-32, 2015.
  • M. Ayala-Rincón, M. Fernández, M.J. Gabbay and A.C. Rocha-Oliveira Checking Overlaps of Nominal Rewriting Rules. Pre-proceedings LSFA 2015:199-2014, 2015. ENTCS 2016 (doi).
  • D. L. Ventura, F. Kamareddine and M. Ayala-Rincón, Explicit substitution calculi with de Bruijn indices and intersection type systems. Logic Journal of the IGPL 23(2): 295-340, 2015. (doi).
  • J.L. Soncco-Álvarez, G.M. Almeida, J. Becker and M. Ayala-Rincón, Parallelization of genetic algorithms for sorting permutations by reversals over biological data. Int. J. Hybrid Intell. Syst. 12(1): 53-64, 2015. (doi).

2014

  • F.L.C. de Moura, D. Kesner and M. Ayala-Rincón Metaconfluence of Calculi with Explicit Substitutions at a Distance, In Proc. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science FST&TCS 2014, LIPIcs Vol. 29 (doi).
  • M. Ayala-Rincón, Tutorial on Fomalization of Rewriting in PVS given in the 7th International School on Rewriting - ISR 2014, Valparaíso Chile, 25 to 29 August 2014.
  • A.B. Avelar, A.L. Galdino, F.L.C. de Moura and M. Ayala-Rincón, First-order unification in the PVS proof assistant, Logic Journal of the IGPL 22(5):758-789, 2014. (doi).
  • D. S. Nogueira Nunes and M. Ayala-Rincón A compressed suffix tree based implementation with low peak memory usage. ENTCS 302:73-94, 2014. (doi).
  • E. H. Haeusler, M. Ayala-Rincón, On the Computability of Relations on λ-Terms and Rice's Theorem - The Case of the Expansion Problem for Explicit Substitutions. LATIN 2014: LNCS, vol. 8392, pages 202-213. (doi).
  • D. M. Muñoz, C. H. Llanos, L. dos Santos Coelho, M. Ayala-Rincón, Hardware opposition-based PSO applied to mobile robot controllers. Engineering Applications of Artificial Intelligence 28:64-77, 2014. (doi)
  • A.A. Almeida, J. Arias-Garcia, C. H. Llanos and M. Ayala-Rincón, Verification of Hardware Implementations through Correctness of Their Recursive Definitions in PVS. ACM Proceedings 27th SBCCI, 2014.
  • J. L. Soncco-Alvarez and M. Ayala-Rincón, Memetic Algorithm for Sorting Unsigned Permutations by Reversals. Proceedings 2014 IEEE Congress on Evolutionary Computation (IEEE CEC 2014), 2014. (doi)

2013

2012

  • D.M. Muñoz-Arboleda, C. H. Llanos, L. Coelho and M. Ayala-Rincón, Accelerating the Artificial Bee Colony Algorithm by Hardware Parallel Implementations. In 3rd IEEE LA Symp. on Circuits and Systems (LASCAS 2012). ((doi))
  • J. Arias-Garcia, C. H. Llanos, M. Ayala-Rincón and R. P. Jacobi A fast and low cost architecture developed in FPGAs for solving systems of linear equations. In 3rd IEEE LA Symp. on Circuits and Systems (LASCAS 2012). ((doi))
  • J. Arias-Garcia, C. H. Llanos, M. Ayala-Rincón and R. P. Jacobi , FPGA implementation of large-scale Matrix Inversion using single, double and custom floating-point precision. In: VIII Southern Conference on Programmable Logic SPL 2012, 2012, IEEE Proc. SPL 2012, 2012. p. 1-6. ((doi))
  • M. Ayala-Rincón Reusing Formal Proofs Through Isomorophisms. Invited Talk LACREST 2012 (PDFs abstract Proc. LACREST 2012 talk ).
  • D. S. Nogueira Nunes and M. Ayala-Rincón A Compressed suffix array based index with succinct longest common prefix information. Short version accepted BSB 2012.
  • A.C. Rocha Oliveira and M. Ayala-Rincón Formalizing the Confluence of Orthogonal Rewriting Systems. Presented in LSFA 2012. EPTCS Vol. 113:145-152, 2013 ((doi), Extended Version, PVS tgz file)
  • D. Nantes Sobrinho, M. Fernández and M. Ayala-Rincón Elementary Deduction Problem for Locally Stable Theories with Normal Forms, PDF. Presented in LSFA 2012. EPTCS Vol. 113:45-60, 2013 ((doi))
  • J.L. Soncco-Álvarez and M. Ayala-Rincón Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations, PDF. Special Issue best papers CLEI 2012, ENTCS Vol. 292:119-133, 2013 ((doi)) .
  • T.A. de Lima and M. Ayala-Rincón Complexity of Reversal Distance and other General Metrics on Permutation Groups, PDF. 7CCC 2012. ((doi))
  • J.L. Soncco-Álvarez and M. Ayala-Rincón A Genetic Approach with a Simple Fitness Function for Sorting Unsigned Permutations by Reversals, Code, PDF. 7CCC 2012. ((doi))

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

  • M. Ayala-Rincón, Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises, chapter in Frontiers of Combining Systems 2 (Studies in Logic and Computation, 7), Dov M. Gabbay and Maarten de Rijke, editors, Research Studies Press/Wiley, 17-38, 1999.
    Click here to order the book at amazon.com.
  • M. Ayala-Rincón and F. Kamareddine, Higher Order Unification via lambda se-Style of Explicit Substitution, Technical Report ULTRA Group ( Useful Logics, Type Theory, Rewriting Systems and Their Applications), CEE, Heriot-Watt University, Edinburgh, Scotland ( Link to ULTRA publications, You will find link to postscript file 600 KB). 53 pages, December 1999.

1998

  • M. Ayala-Rincón and L. M. Gadelha: Some Applications of (Semi-)Decision Algorithms for Presburger Arithmetic in Automated Deduction based on Rewriting Techniques -, in La Revista de la Sociedad Chilena de Ciencia de la Computación , 2(1):14-23 1997 (Edited in June 1998).
  • M. Ayala-Rincón and P. D. Conejo, A Linear Time Lower Bound on Updating Algorithms for Suffix Trees, in Proc. String Processing and Information Retrieval: A South American Symposium, IEEE Computer Society, Santa Cruz de La Sierra, Bolivia. September 1998.
  • M. Ayala-Rincón, Church-Rosser Property for Conditional Rewriting Systems with Built-in Predicates as Premises, in Proc. Frontiers of Combining Systems, Amsterdam, Holland. October 1998. See chapter version in 1999.
  • I. E. T. de Araújo and M. Ayala-Rincón, An Algorithm for General Unification Modulo Presburger Arithmetic, in First Brazilian Workshop on Formal Methods, Porto Alegre, Brasil. October 1998.
  • M. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises, in Revista Colombiana de Matemáticas 31(2):77-98, 1997 (Edited in December 1998).
    See paper in the nearest EMIS mirror: Brasil, Germany or USA.

1997

  • M. Ayala-Rincón: A Deduction Procedure for Conditional Rewriting Systems with Built-in Predicates -, in Proc. SEMISH'97, Brasília, Brasil, August 1997 (Gziped Postscript, 74 KB).
  • L. M. Gadelha and M. Ayala-Rincón: Métodos de Decisão para a Aritmética de Presburger na Dedução Automãtica com Técnicas de Reescrita -, Abstract CNMAC'97 (XX Congresso Nacional de Matemática Aplicada e Computacional), Gramado, Brasil, September 1997 (Gziped Postscript, 24 KB). In Portuguese.
  • L. M. Gadelha and M. Ayala-Rincón: Applications of Decision Algorithms for Presburger Arithmetic in Rewrite Automated Deduction -, in Proc. PANEL'97 (XXIII Latin American Conference on Informatics), Valparaíso, Chile, November 1997 (Gziped Postscript, 56 KB).

1996

  • M. Ayala-Rincón: Fundamentos da Programação Lógica e Funcional - O princípio de resolução e a teoria de reescrita -, Course notes (in Portuguese), Dept. Mathematics, Univ. Brasilia. First version, Jan. 1996; Second version, Dec. 1997; Third version, Dec. 1998; Fourth version, Dec. 2000; Fifth version, March 2001; Sixth version, March 2002; Seventh version March 2003; Eight version, March 2004 (Postscript, 1.6 MB; PDF, 2.2 MB). In Portuguese.
  • M. Ayala-Rincón: Transforming CRSs into TRSs - About Elimination of the Conditions -, in Proc. PANEL'96 (XXII Latin American Conference on Informatics), Bogotá, Colombia, June 1996 (Gziped Postscript, 77 KB).
  • M. Ayala-Rincón: Sistemas de Reescrita de Termos - O Modelo de Computação Funcional e suas Aplicações -, Survey prepared for JAI'96 (XV Jornada de Atualização em Informática do XVI Congresso da Sociedade Brasileira de Computação), Recife, Brasil, August 1996 (Gziped Postscript, 166 KB). In Portuguese.
  • L. M. Gadelha and M. Ayala-Rincón: Aplicação de Métodos de Programação Linear Inteira para Decição na Teoria da Aritmética de Presburger -, Abstract CNMAC'96 (XIX Congresso Nacional de Matemática Aplicada e Computacional), Goiânia, Brasil, September 1996 (Gziped Postscript, 24 KB). In Portuguese.

1995

  • M. Ayala-Rincón: A Note on Confluence of Term Rewriting Systems under Joinability of Critical Pairs in One Step of Parallel Reduction - Abstract, Presented at 11th British Colloquium for Theoretical Computer Science, Swansea, Wales, April 1995 (Compressed Postscript, 23 KB).
  • M. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises, Abstract in Proc. X Latin American Symposium on Mathematical Logic, Bogotá, Colombia, July 1995 (Compressed Postscript, 90 KB).
  • M. Ayala-Rincón: Embedding Built-in Predicates as Premises of Rules of Conditional Rewriting Systems - Abstract, Presented at 2nd Workshop on Logic, Language, Information and Computation, Recife, Brasil, July 1995 (Compressed Postscript, 20 KB). Extended work (submitted) (Gziped Postscript, 100 KB).
  • M. Ayala-Rincón: Confluence of Term Rewriting Systems under Joinability of Critical Pairs in One Step of Parallel Reduction, in Proc. SEMISH-PANEL'95 (XXI Latin American Conference on Informatics), Canela, Brasil, July-August 1995 (Compressed Postscript, 69 KB).
  • M. Ayala-Rincón: A Deductive Calculus for Conditional Equational Systems with Built-in Predicates as Premises - Extended Abstract, in Proc. XV International Conference of the Chilean Computer Science Society, Arica, Chile, October 1995 (Gziped Postscript, 74 KB).
  • M. Ayala-Rincón: Conditional Rewriting Systems with Built-in Predicates and Conjunctions of Standard Premises as Conditions, Technical Report, Dept. Mathematics, Univ. Brasilia, Oct. 1995 (Gziped Postscript, 103 KB).

1994

  • M. Ayala-Rincón: Confluence of Conditional Rewriting Systems with Built-in Predicates and Standard Premises as Conditions, in Proc. SEMISH'94, Caxambú, Brasil, July-August 1994 (Compressed Postscript, 82 KB).

1993

  • M. Ayala-Rincón: Problemas actuales en el campo de la reescritura, in Revista Escuela Colombiana de Ingeniería, 4(10):27-31 January-March 1993. In Spanish
  • M. Ayala-Rincón: Expressiveness of Conditional Equational Systems with Built-in Predicates, PhD thesis under the supervision of Prof. Dr. K. Madlener, Fachbereich Informatik, Universität Kaiserslauten, Germany, December 1993. In English.

ayala NOSP@M mat.unb.br