AbstractsPhilosophy & Theology

Term unification is a basic operation in several areas of computer science, specially in those related to logic. Generally speaking, it consists on solving equations over expressions called terms. Depending on the kind of variables allowed to occur in the terms and under which conditions two terms are considered to be equal, several frameworks of unification such as first-order unification, higher-order unification, syntactic unification, and unification modulo theories can be distinguished. Moreover, other variants of term unification arise when we consider nontrivial representations for terms. In this thesis we study variants of the classic first-order syntactic term unification problem resulting from the introduction of context variables, i.e. variables standing for contexts, and/or assuming that the input is given in some kind of compressed representation. More specifically, we focus on two of such compressed representations: the well-known Directed Acyclic Graphs (DAGs) and Singleton Tree Grammars (STGs). Similarly as DAGs allow compression by exploiting the reusement of repeated instances of a subterm in a term, STGs are a grammar-based compression mechanism based on the reusement of repeated (multi)contexts. An interesting property of the STG formalism is that many operations on terms can be efficiently performed directly in their compressed representation thus taking advantage of the compression also when computing with the represented terms. Although finding a minimal STG representation of a term is computationally difficult, this limitation has been successfully overcome is practice, and several STG-compressors for terms are available. The STG representation has been applied in XML processing and analysis of Term Rewrite Systems. Moreover, STGs are a very useful concept for the analysis of unification problems since, roughly speaking, allow to represent solutions in a succinct but still efficiently verifiable form.; La unificació de termes és una operación básica en diverses àrees de la informática, especialment en aquelles relacionades amb la lógica. En termes generals, consisteix en resoldre equacions sobre expressions anomenades termes. Depenent del tipus de variables que apareguin en els termes i de sota quines condicions dos termes són considerats iguals, podem definir diverses variants del problema d'unificació de termes. A més a més, altres variants del problema d'unificació de termes sorgeixen quan considerem representacions no trivials per als termes. S'estudia variants del problema clàssic d'unificació sintáctica de primer ordre resultants de la introducció de variables de context i/o de l'assumpció de que l'entrada és donada en format comprimit. Ens centrem en l'estudi de dues representacions comprimides: els grafs dirigits acíclics i les gramàtiques d'arbre singletó. Similarment a com els grafs dirigits acíclics permeten compressió mitjançant el reús d'instàncies repetides d'un mateix subterme, les gramàtiques d'arbres singletó són un sistema de compressió basat en el reús de (multi)contexts.…