<HTML>
<HEAD>
<TITLE>Home Page Mauricio Ayala Rinc&oacute;n</TITLE>
</HEAD>

<BODY>


<table>
<td>
<IMG ALIGN=MIDDLE SRC = FotoMAyalaRincon2016.jpg>
</td>
<td>
<H4>
  Mauricio Ayala Rinc&oacute;n, Dr. rer. nat. - <FONT
  COLOR="#FF0000">this is an old page</font> <BR>
  See <FONT COLOR="#FF0000">NEW UPDATED PAGE</FONT> at <a href="https://mayalarincon.github.io">mayalarincon.github.io</a>
<table>
<td> <i>Full Professor</i><br>
<A href="TCgroup/index.html/">Theory of
Computation</a><BR>
Departments of <a href="http://www.cic.unb.br">Computer Science</a> and <a href="https://mat.unb.br/index.php">Mathematics</a> <BR>
Brasilia University</td>
</table>
</H4>
<B>Address:</B><BR>
Departamento de Matem&aacute;tica,  <A HREF="http://www.unb.br">Universidade de Bras&iacute;lia </A><BR>
Campus Universit&aacute;rio Darcy Ribeiro, Asa Norte <BR>
70910-900 Bras&iacute;lia D. F., Brasil<BR>
Tels. +55-61- 3307 2441|2442| +55-61- 3107 6453 | 3676
Fax   +55-61-3273 2737<br>
<B><font color="#FF0000">e-mail:</font></B>
 <A HREF =  "mailto:ayala[at]unb.br">
<I>ayala[at]unb.br</I></A>

<HR>
<table>
<td>
<IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="publications.html"> Publications </A>
<br>
</td>

<td>
 <IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="academics.html">
 Courses </A><br>
</td>
</table>

<table>
<td>
 <IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="pvsclass17/index.html"> PVS
  Class 2017 (affiliated to ITP 2017)</A>
</td> 
<td>  <IMG ALIGN = BOTTON SRC = "ball_red.gif"><a
 HREF="https://thaynaradelima.github.io/Tutorials/UNAL_Manizales_2023"> Mechanizing Mathematics (Tutorial
  UNCOL Manizales, 2023)</a><br>
</td>
</table>

<table>
<td>
<IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="profActivities.html"> Professional Activities </A>
</td>

<td>
<IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="http://buscatextual.cnpq.br/buscatextual/visualizacv.do?metodo=apresentar&id=K4799743E5"> CV Lattes </A>
</td>
</table>

<table>
<td>
<IMG ALIGN = BOTTON SRC = "ball_red.gif"><A HREF="TCgroup/index.html"> Grupo de Teoria da Computa&ccedil;&atilde;o </A>
</td>
</table>


<HR>

<B>Focus of Research:</B><br>
Properties and applications of term rewriting 
 systems and its extensions - 
<A href="links_on_rewriting.html"> Related links</a>
<table>
<td>
<IMG ALIGN = BOTTON SRC = "ball_red.gif"><A
  HREF="http://trs.cic.unb.br"> TRS PVS theory </A> 
<br>
</td>

<td> <IMG ALIGN = BOTTON SRC = "ball_red.gif"><A
  HREF="http://nominal.cic.unb.br"> Nominal PVS theory </A>
  <br>
  </td>
<td>
 <IMG ALIGN = BOTTON SRC = "ball_red.gif"><A
 HREF="http://genoma.cic.unb.br"> Evol. algorithms for sorting permutations </A><br>
</td>
</table>

<!--
<HR>
<H5>
<A HREF="index_portugues.html">Portugu&ecirc;s</A>
<A HREF="index_espaniol.html">Espa&ntilde;ol</A>
</H5>

--> 
</td>
</table>
<HR>


<P><B><FONT COLOR="#000000">Opportunities</FONT></B></P>


<table>
  <td>
<hl>

<li> <FONT COLOR="#FF0000"> Ph.D. scholarships </font>
    Please, enter in contact ASAP, if you are interested in <i>
    Algoritmics, Computational and Mathematical Formalization, Theorem
    Proving, Automated Reasoning, Equational
    and Rewrite-based Deduction, Ethics in AI, Evolutionary and Genetic
    Algorithms, and Genomic Data Processing.</i> 
    
<li> RTA (1983 ... 2015) and TLCA (1993 ... 2015) evolved to
    Int. Conf. on Formal Structures for Computation and Deduction
    <a href="http://fscd-conference.org">FSCD</a> in 2016. <br> <a
    href="https://fscd2025.github.io">FSCD 
    2025</a>, Birmingham, UK.   Deadlines: a:10 Feb, p:17 Feb 2025</a>.  


<li> 27<alt>th</alt> International Conference on Foundations of Software Science and
Computation Structures <a
href="https://etaps.org/2024/conferences/fossacs/">FoSSaCS 2024</a>.
    Luxembourg. Deadline: <a href="https://etaps.org/2024/cfp/">12 Oct
    2023</a>.

<li> 18th Conference on Intelligent Computer Mathematics <a
    href="https://cicm-conference.org/2025/cicm.php">CICM 2025</a>,
    Bras&iacute;lia, 
    6-11 Oct 2025  (CICM + LSFA). Deadlines: a:28
    Abr, p:5 May 2025.
    
<li> 20th Logical and Semantic Frameworks, with Applications <a
    href="https://lsfa-workshop.github.io/2025">LSFA 2025</a>,
    Bras&iacute;lia, 6-11 Oct 2025  (CICM + LSFA)

<li> The 17th NASA Formal Methods Symposium <a
    href="https://shemesh.larc.nasa.gov/nfm2025/">NFM 2025</a>,
    Williamsburg VA, (NFM).  a:13 Dec, p:22 Dec 2024    

<li> International Conference on Interactive Theorem Proving <a
href="https://itp-conference.github.io">ITP web page</a>.  <a
    href="https://icetcs.github.io/frocos-itp-tableaux25/">ITP
    2025</a>, Reykjavik, Iceland.  

<li> 14<sup>th</sup> International Workshop on Confluence <a
    href="http://cl-informatik.uibk.ac.at/iwc">IWC 2025</a>, Lepzig,
    Germany.  

<li> 37<sup>th</sup> International Workshop on Unification <a
    href="https://lat.inf.tu-dresden.de/unif2024/">UNIF 2024</a>, 
    Co-located with IJCAR 2024, Nancy, France.    
    
    <li> <a href="TCgroup/events.html"> Recent Talks at
    GTC/UnB</a>: <b> Track on Logic and Computation</b> (<a
    href="EVENTS/Th_Comp_Summer_Workshop_UnB_2024.pdf"> Final Progam</a>), part of the XVL SW in
    Mathematics (UnB) - <b>(7-9 February, 2024)</b>
  

<br>
</hl>
</td>

<td>
  <IMG ALIGN=MIDDLE SRC = capaflogfun.jpg width="75mm" >
  <br> <br>
  
   <IMG ALIGN=MIDDLE SRC = UTCS.jpg width="75mm">
</td>
<td>
<B><FONT COLOR="#000000">M. Ayala-Rinc&oacute;n & Fl&aacute;vio
L.C. de Moura, <I> <a href="https://loja.editora.unb.br/engenharia/fundamentos-da-programacao-logica-e-funcional--o-principio-de-resolucao-e-a-teoria-de-reescrita-742/p">Fundamentos
da Programa&ccedil;&atilde;o L&oacute;gica e Funcional - O Princ&iacute;pio
de Resolu&ccedil;&atilde;o e a Teoria de Reescrita</a> -,</I> Course
  Notes, Ed. UnB, December 2014.  In Portuguese.</FONT></B>
  <br> <br> <br>
  <B><FONT COLOR="#000000">M. Ayala-Rinc&oacute;n & Fl&aacute;vio
L.C. de Moura, <I> <a
  href="http://www.springer.com/gb/book/9783319516516#aboutBook">Applied
  Logic for Computer Scientists:
  Computational Deduction and Formal Proofs</a>,</I> Springer, 2017.</FONT></B>
</td>


  </table>

<P>

<HR>


<ADDRESS>
<DT><A HREF =  "mailto:ayala[at]unb.br">
<I>ayala[at]unb.br</I></P></A>
</ADDRESS>

</BODY>
</HTML>