Graphic summary
  • Show / hide key
  • Information


Scientific and technological production
  •  

1 to 48 of 48 results
  • Excessively duplicating patterns represent non-regular languages

     Creus Lopez, Carles; Godoy Balil, Guillermo; Ramos Garrido, Lander
    Information processing letters
    Vol. 114, num. 3, p. 85-93
    DOI: 10.1016/j.ipl.2013.11.010
    Date of publication: 2014-03-01
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    A constrained term pattern s:¿ represents the language of all instances of the term s satisfying the constraint ¿. For each variable in s, this constraint specifies the language of its allowed substitutions. Regularity of languages represented by sets of patterns has been studied for a long time. This problem is known to be co-NP-complete when the constraints allow each variable to be replaced by any term over a fixed signature, and EXPTIME-complete when the constraints restrict each variable to a regular set. In both cases, duplication of variables in the terms of the patterns is a necessary condition for non-regularity. This is because duplications force the recognizer to test equality between subterms. Hence, for the specific classes of constraints mentioned above, if all patterns are linear, then the represented language is necessarily regular. In this paper we focus on the opposite case, that is when there are patterns with "excessively duplicating" variables. We prove that when each pattern of a non-empty set has a duplicated variable constrained to an infinite language, then the language represented by the set is necessarily non-regular. We prove this result independently of the kind of constraints used, just assuming that they are mappings from variables to arbitrary languages. Our result provides an efficient procedure for detecting, in some cases, non-regularity of images of regular languages under tree homomorphisms

    A constrained term pattern s:¿ represents the language of all instances of the term s satisfying the constraint ¿. For each variable in s, this constraint specifies the language of its allowed substitutions. Regularity of languages represented by sets of patterns has been studied for a long time. This problem is known to be co-NP-complete when the constraints allow each variable to be replaced by any term over a fixed signature, and EXPTIME-complete when the constraints restrict each variable to a regular set. In both cases, duplication of variables in the terms of the patterns is a necessary condition for non-regularity. This is because duplications force the recognizer to test equality between subterms. Hence, for the specific classes of constraints mentioned above, if all patterns are linear, then the represented language is necessarily regular. In this paper we focus on the opposite case, that is when there are patterns with

  • Modelos y métodos computacionales para datos masivos estructurados

     Diaz Cort, Jose Maria; Cortadella Fortuny, Jordi; Serna Iglesias, Maria Jose; Alvarez Faura, Maria Del Carme; Pino Blanco, Elvira Patricia; Carmona Vargas, Jose; Gabarro Valles, Joaquin; Xhafa Xhafa, Fatos; Pasarella Sanchez, Ana Edelmira; Petit Silvestre, Jordi; Mylonakis Pascual, Nicolas Eduardo; Martinez Parra, Conrado; Duch Brown, Amalia; Godoy Balil, Guillermo; Roura Ferret, Salvador; Roca Perez, Antoni; Soares Ribeiro, Joel Tiago; Pérez Giménez, Xavier; Orejas Valdes, Fernando
    Competitive project

     Share

  • Variants of unification considering compression and context variables

     Gascon Caro, Adrian
    Universitat Politècnica de Catalunya
    Theses

    Read the abstract Read the abstract  Share Reference managers Reference managers Open in new window

    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. Una propietat interessant d¿aquest formalisme és que moltes de les operacions comuns sobre termes es poden realizar directament sobre la versió comprimida d¿aquests de forma eficient, sense cap mena de descompressió prèvia. Tot i que trobar una representació minimal d¿un terme amb una gramática singletó és una tasca computacionalment difícil, aquesta limitació ha estat resolta de forma satisfactòria en la pràctica, hi ha disponibles diversos compressors per a termes. La representació de termes amb gramàtiques singletó ha estat útil per al processament de documents XML i l¿anàlisi de sistemes de reescriptura de termes. Les gramàtiques singletó són concepte molt útil per a l¿anàlisi de problemas d¿unificació, ja que permeten representar solucions de forma comprimida sense renunciar a que puguin ser verificades de forma eficient.A la primera part d¿aquesta tesi s¿estudien els problemas d¿unificació i matching de primer ordre sota l¿assumpció de que els termes de l¿entrada són representats fent servir gramàtiques singletó. Presentem algorismes de temps polinòmic per a aquests problemas, així com propostes d¿implementacions i resultats experimentals. Aquests resultats s¿utilitzen més endevant en aquesta tesi per a l¿anàlisi de problemes d¿unificació i matching amb variables de contexte i entrada comprimida.A la resta d¿aquesta tesi ens centrem en variants d¿unificació amb variables de contexte, que són un cas particular de variables d¿ordre superior. Més concretament, a la segona part d¿aquesta tesi, ens centrem en un cas particular d¿unificació de contextes on nomès es permet una sola variable de context en l¿entrada. Aquest problema s¿anomena ¿one context unification¿. Mostrem que aquest problema es pot resoldre en temps polinòmic indeterminista, no només quan els termes de l¿entrada són representats de forma explícita, sino també quan es representen fent servir grafs dirigits acíclics i gramàtiques singletó. També presentem un resultat parcial recent en la tasca de trobar un algorisme de temps polinòmic per a one context unification.Al final de la tesi, estudiem el problema de matching per a entrades amb variables de contexte, que és un cas particular d¿unificació on només un dels dos termes de cada equació té variables. En contrast amb el problema general, matching de contextes ha estat classificat com a problema NP-complet. Mostrem que matching de contextes és NP-complet fins i tot quan es fan servir gramàtiques com a formalisme de representació de termes. Això implica que afegir compressió no ens porta a un augment dràstic de la complexitat del problema. També demostrem que la restricció de matching de contextes on el nombre de variables de contexte està afitat per una constant fixa del problema es pot resoldre en temps polinòmic, fins i tot quan es fan servir grafs dirigits acíclics com formalisme de representació de termes.

  • Automatic evaluation of reductions between NP-complete problems

     Creus Lopez, Carles; Fernandez Duran, Pablo; Godoy Balil, Guillermo
    International Conference on Theory and Applications of Satisfiability Testing
    p. 415-421
    DOI: 10.1007/978-3-319-09284-3_30
    Presentation's date: 2014-07-14
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We implement an online judge for evaluating correctness of reductions between NP-complete problems. The site has a list of exercises asking for a reduction between two given problems. Internally, the reduction is evaluated by means of a set of tests. Each test consists of an input of the first problem and gives rise to an input of the second problem through the reduction. The correctness of the reduction, that is, the preservation of the answer between both problems, is checked by applying additional reductions to SAT and using a state-of-the-art SAT solver. In order to represent the reductions, we have defined a new programming language called REDNP. On one side, REDNP has specific features for describing typical concepts that frequently appear in reductions, like graphs and clauses. On the other side, we impose severe limitations to REDNP in order to avoid malicious submissions, like the ones with an embedded SAT solver.

    We implement an online judge for evaluating correctness of reductions between NP-complete problems. The site has a list of exercises asking for a reduction between two given problems. Internally, the reduction is evaluated by means of a set of tests. Each test consists of an input of the first problem and gives rise to an input of the second problem through the reduction. The correctness of the reduction, that is, the preservation of the answer between both problems, is checked by applying additional reductions to SAT and using a state-of-the-art SAT solver. In order to represent the reductions, we have defined a new programming language called REDNP. On one side, REDNP has specific features for describing typical concepts that frequently appear in reductions, like graphs and clauses. On the other side, we impose severe limitations to REDNP in order to avoid malicious submissions, like the ones with an embedded SAT solver.

  • Automatic evaluation of context-free grammars (system description)

     Creus Lopez, Carles; Godoy Balil, Guillermo
    International Conference on Rewriting Techniques and Applications
    p. 139-148
    DOI: 10.1007/978-3-319-08918-8-10
    Presentation's date: 2014-07-14
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We implement an online judge for context-free grammars. Our system contains a list of problems describing formal languages, and asking for grammars generating them. A submitted proposal grammar receives a verdict of acceptance or rejection depending on whether the judge determines that it is equivalent to the reference solution grammar provided by the problem setter. Since equivalence of context-free grammars is an undecidable problem, we consider a maximum length l and only test equivalence of the generated languages up to words of length l. This length restriction is very often sufficient for the well-meant submissions. Since this restricted problem is still NP-complete, we design and implement methods based on hashing, SAT, and automata that perform well in practice. © 2014 Springer International Publishing Switzerland.

    We implement an online judge for context-free grammars. Our system contains a list of problems describing formal languages, and asking for grammars generating them. A submitted proposal grammar receives a verdict of acceptance or rejection depending on whether the judge determines that it is equivalent to the reference solution grammar provided by the problem setter. Since equivalence of context-free grammars is an undecidable problem, we consider a maximum length l and only test equivalence of the generated languages up to words of length l. This length restriction is very often sufficient for the well-meant submissions. Since this restricted problem is still NP-complete, we design and implement methods based on hashing, SAT, and automata that perform well in practice. © 2014 Springer International Publishing Switzerland.

  • Tree automata with height constraints between brothers

     Creus Lopez, Carles; Godoy Balil, Guillermo
    International Conference on Rewriting Techniques and Applications
    p. 149-163
    DOI: 10.1007/978-3-319-08918-8-11
    Presentation's date: 2014-07-14
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We define the tree automata with height constraints between brothers (TACBB H ). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in TACBB H. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for TACBB H, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers. © 2014 Springer International Publishing Switzerland.

    We define the tree automata with height constraints between brothers (TACBB H ). Constraints of equalities and inequalities between heights of siblings that restrict the applicability of the rules are allowed in TACBB H. These constraints allow to express natural tree languages like complete or balanced (like AVL) trees. We prove decidability of emptiness and finiteness for TACBB H, and also for a more general class that additionally allows to combine equality and disequality constraints between brothers. © 2014 Springer International Publishing Switzerland.

  • Emptiness and finiteness for tree automata with global reflexive disequality constraints

     Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo
    Journal of automated reasoning
    Vol. 51, num. 4, p. 371-400
    DOI: 10.1007/s10817-012-9270-5
    Date of publication: 2013-12-01
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    In recent years, several extensions of tree automata have been considered. Most of them are related with the capability of testing equality or disequality of certain subterms of the term evaluated by the automaton. In particular, tree automata with global constraints are able to test equality and disequality of subterms depending on the state to which they are evaluated. The emptiness problem is known decidable for this kind of automata, but with a non-elementary time complexity, and the finiteness problem remains unknown. In this paper, we consider the particular case of tree automata with global constraints when the constraint is a conjunction of disequalities between states, and the disequality predicate is forced to be reflexive. This restriction is significant in the context of XML definitions with monadic key constraints. We prove that emptiness and finiteness are decidable in triple exponential time for this kind of automata. © 2012 Springer Science+Business Media Dordrecht.

    In recent years, several extensions of tree automata have been considered. Most of them are related with the capability of testing equality or disequality of certain subterms of the term evaluated by the automaton. In particular, tree automata with global constraints are able to test equality and disequality of subterms depending on the state to which they are evaluated. The emptiness problem is known decidable for this kind of automata, but with a non-elementary time complexity, and the finiteness problem remains unknown. In this paper, we consider the particular case of tree automata with global constraints when the constraint is a conjunction of disequalities between states, and the disequality predicate is forced to be reflexive. This restriction is significant in the context of XML definitions with monadic key constraints. We prove that emptiness and finiteness are decidable in triple exponential time for this kind of automata. © 2012 Springer Science+Business Media Dordrecht.

  • Non-linear rewrite closure and weak normalization

     Creus Lopez, Carles; Godoy Balil, Guillermo; Massanes Basi, Francesc d'Assis; Tiwari, Ashish Kumar
    Journal of automated reasoning
    Vol. 51, num. 3, p. 281-324
    DOI: 10.1007/s10817-012-9262-5
    Date of publication: 2013-10
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    A rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. Rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. This property has been useful for proving decidability results in term rewriting. Unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). The left-hand side term is unrestricted, and in particular, it may be non-linear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that right-shallow right-linear term rewrite systems are regularity preserving. Moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. A preliminary version of this work was presented at LICS 2009.

    A rewrite closure is an extension of a term rewrite system with new rules, usually deduced by transitivity. Rewrite closures have the nice property that all rewrite derivations can be transformed into derivations of a simple form. This property has been useful for proving decidability results in term rewriting. Unfortunately, when the term rewrite system is not linear, the construction of a rewrite closure is quite challenging. In this paper, we construct a rewrite closure for term rewrite systems that satisfy two properties: the right-hand side term in each rewrite rule contains no repeated variable (right-linear) and contains no variable occurring at depth greater than one (right-shallow). The left-hand side term is unrestricted, and in particular, it may be non-linear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for right-linear right-shallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that right-shallow right-linear term rewrite systems are regularity preserving. Moreover, their set of normal forms can be represented with a tree automaton with disequality constraints, and emptiness of this kind of automata, as well as its generalization to reduction automata, is decidable. A preliminary version of this work was presented at LICS 2009.

  • Access to the full text
    Decidable classes of tree automata mixing local and global constraints modulo flat theories  Open access

     Barguño, Luis; Creus Lopez, Carles; Godoy Balil, Guillermo; Jacquemard, Florent; Vacher, Camile
    Logical methods in computer science
    Vol. 9, num. 2, p. 1-39
    DOI: 10.2168/LMCS-9(2:01)2013
    Date of publication: 2013-02
    Journal article

    Read the abstract Read the abstract Access to the full text Access to the full text Open in new window  Share Reference managers Reference managers Open in new window

    We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TABG. This solves, in particular, the open question of the decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.

    We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TABG. This solves, in particular, the open question of the decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.

  • The HOM problem is EXPTIME-complete

     Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo; Ramos, Lander
    IEEE Logic in Computer Science
    p. 255-264
    DOI: 10.1109/LICS.2012.36
    Presentation's date: 2012
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    The HOM problem questions whether the image of a given regular tree language through a given tree homomorphism is also regular. Decidability of HOM is an important theoretical question which was open for a long time. Recently, HOM has been proved decidable with a triple exponential time algorithm. In this paper we obtain an exponential time algorithm for this problem, and conclude that it is EXPTIME-complete. The proof builds upon previous results and techniques on tree automata with constraints.

  • Sweetlogics-UPC

     Nivela Alos, Mª Del Pilar Brigida; Valles Fuente, Borja; Messeguer Peypoch, Xavier; Oliveira Neto, Alexandre Francisco; Abío Roig, Ignasi; Asín Acha, Roberto Javier; Godoy Balil, Guillermo; Rivero Almeida, Jose Miguel; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
    Competitive project

     Share

  • Unification and matching on compressed terms

     Gascon Caro, Adrian; Godoy Balil, Guillermo; Schmidt-Schauß, Manfred
    ACM transactions on computational logic
    Vol. 12, num. 4, p. 1-42
    DOI: 10.1145/1970398.1970402
    Date of publication: 2011-07-29
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    Term unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammar-based compression for terms, in particular the so-called singleton tree grammars (STGAs), have recently drawn considerable attention. Using STGs, terms of exponential size and height can be represented in linear space. Furthermore, the term representation by directed acyclic graphs (dags) can be efficiently simulated. The present article is the result of an investigation on term unification and matching when the terms given as input are represented using different compression mechanisms for terms such as dags and singleton tree grammars. We describe a polynomial time algorithm for context matching with dags, when the number of different context variables is fixed for the problem. For the same problem, NP-completeness is obtained when the terms are represented using the more general formalism of singleton tree grammars. For first-order unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems.

  • Deciding regularity of the set of instances of a set of terms with regular constraints is EXPTIME-Complete

     Gimenez Llach, Omer; Godoy Balil, Guillermo; Maneth, Sebastian
    SIAM journal on computing
    Vol. 40, num. 2, p. 446-464
    DOI: 10.1137/090777669
    Date of publication: 2011
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Learning theory through videos: a teaching experience in a theoretical course based on self-learning videos and problem-solving sessions

     Arias Vicente, Marta; Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo
    International Conference on Computer Supported Education
    p. 93-98
    DOI: 10.5220/0003333400930098
    Presentation's date: 2011-05
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • The HOM problem is decidable

     Godoy Balil, Guillermo; Gimenez Llach, Omer; Ramos, Lander; Alvarez Faura, Maria Del Carme
    ACM Symposium on Theory of Computing
    p. 485-494
    DOI: 10.1145/1806689.1806757
    Presentation's date: 2010
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Termination of rewriting with right-flat rules modulo permutative theories

     Barguño Jané, Luis; Godoy Balil, Guillermo; Huntingford, Eduard; Tiwari, Ashish
    Logical methods in computer science
    Vol. 6, num. 3, p. 1-20
    DOI: 10.2168/LMCS-6(3:8)2010
    Date of publication: 2010
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Context unification with one context variable

     Gascon Caro, Adrian; Godoy Balil, Guillermo; Schmidt-Schauß, Manfred; Tiwari, Ashish
    Journal of symbolic computation
    Vol. 45, num. 2, p. 173-193
    DOI: 10.1016/j.jsc.2008.10.005
    Date of publication: 2010-02
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Normalization properties for Shallow TRS and Innermost Rewriting

     Godoy Balil, Guillermo
    Applicable algebra in engineering communication and computing
    Vol. 21, num. 2, p. 109-129
    DOI: 10.1007/s00200-009-0118-0
    Date of publication: 2010-03
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • The emptiness problem for tree automata with global constraints

     Barguño Jané, Luis; Creus Lopez, Carles; Godoy Balil, Guillermo; Jacquemard, Florent; Vacher, Camille
    IEEE Logic in Computer Science
    p. 263-272
    DOI: 10.1109/LICS.2010.28
    Presentation's date: 2010
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • ALGORISMIA, BIOINFORMÀTICA, COMPLEXITAT I METODES FORMALS (ALBCOM)

     Orejas Valdes, Fernando; Galceran Oms, Marc; Oliva Valls, Sergi; Godoy Balil, Guillermo; Atserias Peri, Albert; Martinez Parra, Conrado; Pasarella Sanchez, Ana Edelmira; Pino Blanco, Elvira Patricia; Alvarez Faura, Maria Del Carme; Blum, Christian Clemens; Gabarro Valles, Joaquin; Cortadella Fortuny, Jordi; Molinero Albareda, Xavier; Serna Iglesias, Maria Jose; Messeguer Peypoch, Xavier; Roura Ferret, Salvador; Blesa Aguilera, Maria Jose; Valiente Feruglio, Gabriel Alejandro; Duch Brown, Amalia; Carmona Vargas, Jose; Hernandez Pibernat, Hugo; Gel Moreno, Bernat; Gascon Caro, Adrian; Petit Silvestre, Jordi; Diaz Cort, Jose Maria
    Competitive project

     Share

  • Undecidable properties of flat term rewrite systems

     Godoy Balil, Guillermo; Hernandez Pibernat, Hugo
    Applicable algebra in engineering communication and computing
    Vol. 20, num. 2, p. 187-205
    Date of publication: 2009-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Closure of Tree Automata Languages under Innermost Rewriting

     Gascon Caro, Adrian; Godoy Balil, Guillermo; Jacquemard, F
    Electronic notes in theoretical computer science
    Vol. 237, p. 23-38
    Date of publication: 2009-04
    Journal article

     Share Reference managers Reference managers Open in new window

  • Métodos formales y algoritmos para el diseño de sistemas

     Xhafa Xhafa, Fatos; Orejas Valdes, Fernando; Godoy Balil, Guillermo; Costa Gorgônio, Kyller; Oliva Valls, Sergi; Galceran Oms, Marc; Gascon Caro, Adrian; Gel Moreno, Bernat; Hernandez Pibernat, Hugo; Duch Brown, Amalia; Blum, Christian Clemens; Pasarella Sanchez, Ana Edelmira; Diaz Cort, Jose Maria; Pino Blanco, Elvira Patricia; Petit Silvestre, Jordi; Alvarez Faura, Maria Del Carme; Blesa Aguilera, Maria Jose; Gabarro Valles, Joaquin; Cortadella Fortuny, Jordi; Serna Iglesias, Maria Jose; Carmona Vargas, Jose
    Competitive project

     Share

  • On the Normalization and Unique Normalization Properties of Term Rewrite Systems

     Godoy Balil, Guillermo; Sophie, Tison
    CADE-21, 21st International Conference on Automated Deduction
    p. 247-262
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Innermost-Reachability and Innermost-Joinability Are Decidable for Shallow Term Rewrite Systems

     Godoy Balil, Guillermo; Huntingford, Eduard
    Term Rewriting and Applications, 18th International Conference, RTA 2007
    p. 184-199
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Termination of Rewriting with Right-Flat Rules

     Godoy Balil, Guillermo; Huntingford, Eduard; Ashish, Tiwari
    Term Rewriting and Applications, 18th International Conference, RTA 2007
    p. 200-213
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • TERMINATION OF REWRITING WITH MON-MONOTONIC ORDERING

     FERNANDEZ VENERO, MIRTHA LINA
    Department of Computer Science, Universitat Politècnica de Catalunya
    Theses

     Share Reference managers Reference managers Open in new window

  • Orderings for Innermost Termination

     Mirtha-Lina, Fernández; Godoy Balil, Guillermo; Rubio Gimeno, Alberto
    Lecture notes in computer science
    Vol. 3467, p. 17-31
    Date of publication: 2005-04
    Journal article

     Share Reference managers Reference managers Open in new window

  • Recursive Path Orderings Can Also Be Incremental

     Mirtha-Lina, Fernández; Godoy Balil, Guillermo; Rubio Gimeno, Alberto
    Lecture notes in computer science
    Vol. 3835, p. 230-245
    Date of publication: 2005-12
    Journal article

     Share Reference managers Reference managers Open in new window

  • Confluence of Shallow Right-Linear Rewrite Systems

     Godoy Balil, Guillermo; Ashish, Tiwari
    Lecture notes in computer science
    Vol. 3634, p. 541-556
    Date of publication: 2005-08
    Journal article

     Share Reference managers Reference managers Open in new window

  • Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules

     Godoy Balil, Guillermo; Ashish, Tiwari
    Lecture notes in computer science
    Vol. 3632, p. 164-176
    Date of publication: 2005-07
    Journal article

     Share Reference managers Reference managers Open in new window

  • Superposition with completely built-in Abelian groups

     Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
    Journal of symbolic computation
    Vol. 37, num. 1, p. 1-33
    Date of publication: 2004-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Characterizing Confluence by Rewrite Closure and Right Ground Term Rewrite Systems

     Godoy Balil, Guillermo; Ashish, Tiwari; Rakesh, M Verma
    Applicable algebra in engineering communication and computing
    Vol. 15, num. 1, p. 13-36
    Date of publication: 2004-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Deciding Fundamental Properties of Right-(Ground or Variable) Rewrite Systems by Rewrite Closure

     Godoy Balil, Guillermo; Ashish, Tiwari
    Lecture notes in computer science
    Vol. 3097, p. 91-106
    Date of publication: 2004-07
    Journal article

     Share Reference managers Reference managers Open in new window

  • Classes of term rewrite systems with polynomial confluence problems

     Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Ashish, Tiwari
    ACM transactions on computational logic
    Vol. 5, num. 2, p. 321-331
    Date of publication: 2004-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups

     Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
    Constraints
    Vol. 9, num. 3, p. 167-192
    Date of publication: 2004-07
    Journal article

     Share Reference managers Reference managers Open in new window

  • Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings

     Miquel, Bofill; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
    Journal of automated reasoning
    Vol. 30, num. 1, p. 99-120
    Date of publication: 2003-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • On the Confluence of Linear Shallow Term Rewrite Systems

     Godoy Balil, Guillermo; Ashish, Tiwari; Rakesh, M Verma
    Lecture notes in computer science
    Vol. 2607, p. 85-96
    Date of publication: 2003-03
    Journal article

     Share Reference managers Reference managers Open in new window

  • Programa de acción en aprendizaje cooperativo

     Abello Gamazo, Alberto; Domingo Peña, Joan; Florido Pérez, Antonio; Godoy Balil, Guillermo; Gómez, J; Gorchs Altarriba, Roser; Martínez, M; Romera Diez, Pedro Luis; Usandizaga Calparsoro, Miguel M.
    Jornada sobre Aprendizaje Cooperativo
    p. 7-8
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • On Ordering Constraints For Deduction with Built-In Abelian Semigroups, Monoids and Groups

     Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
    16th Annual IEEE Symposium on Logic in Computer Science (LICS)
    p. 38-47
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time

     Comon, H G Godoy; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
    42nd Annual Symposium on Foundations of Computer Science (FOCS)
    p. 298-307
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Automated Deduction with Built-in Theories. Completeness Results and Constraint Solving Techniques.

     Godoy Balil, Guillermo
    Department of Computer Science, Universitat Politècnica de Catalunya
    Theses

     Share Reference managers Reference managers Open in new window

  • On the Completeness of Arbitrary Selection Strategies for Paramodulation

     Bofill, M; Godoy Balil, Guillermo
    Lecture notes in computer science
    Vol. 2076, p. 951-962
    Date of publication: 2001-07
    Journal article

     Share Reference managers Reference managers Open in new window

  • Modular Redundancy for Theorem Proving

     Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
    Int. Conf. on Frontiers of Combining Systems
    p. 186-199
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Paramodulation with Built-in Abelian Groups

     Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
    15th Annual IEEE Symposium on Logic nin Computer Science (LICS)
    p. 337-348
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Modular Redundancy for Theorem Proving

     Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
    Lecture notes in computer science
    Vol. 1794, p. 186-199
    Date of publication: 2000-03
    Journal article

     Share Reference managers Reference managers Open in new window

  • Paramodulation with non-Monotonic Orderings

     Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
    Fourteenth annual IEEE Symposium on Logic in Computer Science
    p. 225-233
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window