 Research group
 ALBCOM  Algorithms, Computational Biology, Complexity and Formal Methods
 Department
 Department of Software
 School
 Barcelona School of Informatics (FIB)
 ggodoylsi.upc.edu
 Contact details
 UPC directory
Scientific and technological production


Nonlinear rewrite closure and weak normalization
Creus Lopez, Carles; Godoy Balil, Guillermo; Massanes Basi, Francesc d'Assis; Tiwari, Ashish Kumar
Journal of automated reasoning
Date of publication: 201310
Journal article
Read the abstract View Share Reference managersA 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 righthand side term in each rewrite rule contains no repeated variable (rightlinear) and contains no variable occurring at depth greater than one (rightshallow). The lefthand side term is unrestricted, and in particular, it may be nonlinear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for rightlinear rightshallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that rightshallow rightlinear 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 righthand side term in each rewrite rule contains no repeated variable (rightlinear) and contains no variable occurring at depth greater than one (rightshallow). The lefthand side term is unrestricted, and in particular, it may be nonlinear. As a consequence of the rewrite closure construction, we are able to prove decidability of the weak normalization problem for rightlinear rightshallow term rewrite systems. Proving this result also requires tree automata theory. We use the fact that rightshallow rightlinear 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. 
Decidable classes of tree automata mixing local and global constraints modulo flat theories
Barguño, Luis; Creus Lopez, Carles; Godoy Balil, Guillermo; Jacquemard, Florent; Vacher, Camile
Logical methods in computer science
Date of publication: 201302
Journal article
Read the abstract Access to the full text Share Reference managersWe 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 EXPTIMEcomplete
Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo; Ramos, Lander
IEEE Logic in Computer Science
Presentation's date: 2012
Presentation of work at congresses
Read the abstract View Share Reference managersThe 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 EXPTIMEcomplete. The proof builds upon previous results and techniques on tree automata with constraints. 
Learning theory through videos: a teaching experience in a theoretical course based on selflearning videos and problemsolving sessions
Arias Vicente, Marta; Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo
International Conference on Computer Supported Education
Presentation's date: 201105
Presentation of work at congresses
View Share Reference managers 
Deciding regularity of the set of instances of a set of terms with regular constraints is EXPTIMEComplete
Gimenez Llach, Omer; Godoy Balil, Guillermo; Maneth, Sebastian
SIAM journal on computing
Date of publication: 2011
Journal article
View Share Reference managers 
Unification and matching on compressed terms
Gascon Caro, Adrian; Godoy Balil, Guillermo; SchmidtSchauß, Manfred
ACM transactions on computational logic
Date of publication: 20110729
Journal article
Read the abstract View Share Reference managersTerm unification plays an important role in many areas of computer science, especially in those related to logic. The universal mechanism of grammarbased compression for terms, in particular the socalled 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, NPcompleteness is obtained when the terms are represented using the more general formalism of singleton tree grammars. For firstorder unification and matching polynomial time algorithms are presented, each of them improving previous results for those problems. 
SweetlogicsUPC
Messeguer Peypoch, Xavier; Godoy Balil, Guillermo; Asín Acha, Roberto Javier; Abío Roig, Ignasi; Oliveira Neto, Alexandre Francisco; Valles Fuente, Borja; Nivela Alos, Mª Del Pilar Brigida; Rivero Almeida, Jose Miguel; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto
Participation in a competitive project
Share 
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
Presentation's date: 2010
Presentation of work at congresses
View Share Reference managers 
The HOM problem is decidable
Godoy Balil, Guillermo; Gimenez Llach, Omer; Ramos, Lander; Alvarez Faura, Maria Del Carme
ACM Symposium on Theory of Computing
Presentation's date: 2010
Presentation of work at congresses
View Share Reference managers 
Normalization properties for Shallow TRS and Innermost Rewriting
Godoy Balil, Guillermo
Applicable algebra in engineering communication and computing
Date of publication: 201003
Journal article
View Share Reference managers 
Context unification with one context variable
Gascon Caro, Adrian; Godoy Balil, Guillermo; SchmidtSchauß, Manfred; Tiwari, Ashish
Journal of symbolic computation
Date of publication: 201002
Journal article
View Share Reference managers 
Termination of rewriting with rightflat rules modulo permutative theories
Barguño Jané, Luis; Godoy Balil, Guillermo; Huntingford, Eduard; Tiwari, Ashish
Logical methods in computer science
Date of publication: 2010
Journal article
View Share Reference managers 
Closure of Tree Automata Languages under Innermost Rewriting
Gascon Caro, Adrian; Godoy Balil, Guillermo; Jacquemard, F
Electronic notes in theoretical computer science
Date of publication: 200904
Journal article
Share Reference managers 
Algorismia, bioinformàtica, complexitat i mètodes 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; 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
Participation in a competitive project
Share 
Undecidable properties of flat term rewrite systems
Godoy Balil, Guillermo; Hernandez Pibernat, Hugo
Applicable algebra in engineering communication and computing
Date of publication: 200901
Journal article
Share Reference managers 
TERMINATION OF REWRITING WITH MONMONOTONIC ORDERING
FERNANDEZ VENERO, MIRTHA LINA
Defense's date: 20070523
Department of Software, Universitat Politècnica de Catalunya
Theses
Share Reference managers 
On the Normalization and Unique Normalization Properties of Term Rewrite Systems
Godoy Balil, Guillermo; Sophie, Tison
CADE21, 21st International Conference on Automated Deduction
Presentation of work at congresses
Share Reference managers 
InnermostReachability and InnermostJoinability Are Decidable for Shallow Term Rewrite Systems
Godoy Balil, Guillermo; Huntingford, Eduard
Term Rewriting and Applications, 18th International Conference, RTA 2007
Presentation of work at congresses
Share Reference managers 
Termination of Rewriting with RightFlat Rules
Godoy Balil, Guillermo; Huntingford, Eduard; Ashish, Tiwari
Term Rewriting and Applications, 18th International Conference, RTA 2007
Presentation of work at congresses
Share Reference managers 
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; 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
Participation in a competitive project
Share 
Orderings for Innermost Termination
MirthaLina, Fernández; Godoy Balil, Guillermo; Rubio Gimeno, Alberto
Lecture notes in computer science
Date of publication: 200504
Journal article
Share Reference managers 
Recursive Path Orderings Can Also Be Incremental
MirthaLina, Fernández; Godoy Balil, Guillermo; Rubio Gimeno, Alberto
Lecture notes in computer science
Date of publication: 200512
Journal article
Share Reference managers 
Confluence of Shallow RightLinear Rewrite Systems
Godoy Balil, Guillermo; Ashish, Tiwari
Lecture notes in computer science
Date of publication: 200508
Journal article
Share Reference managers 
Termination of Rewrite Systems with Shallow RightLinear, Collapsing, and RightGround Rules
Godoy Balil, Guillermo; Ashish, Tiwari
Lecture notes in computer science
Date of publication: 200507
Journal article
Share Reference managers 
Superposition with completely builtin Abelian groups
Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
Journal of symbolic computation
Date of publication: 200401
Journal article
Share Reference managers 
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
Date of publication: 200401
Journal article
Share Reference managers 
Deciding Fundamental Properties of Right(Ground or Variable) Rewrite Systems by Rewrite Closure
Godoy Balil, Guillermo; Ashish, Tiwari
Lecture notes in computer science
Date of publication: 200407
Journal article
Share Reference managers 
Classes of term rewrite systems with polynomial confluence problems
Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Ashish, Tiwari
ACM transactions on computational logic
Date of publication: 200401
Journal article
Share Reference managers 
Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups
Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
Constraints
Date of publication: 200407
Journal article
Share Reference managers 
Paramodulation and KnuthBendix Completion with Nontotal and Nonmonotonic Orderings
Miquel, Bofill; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
Journal of automated reasoning
Date of publication: 200301
Journal article
Share Reference managers 
On the Confluence of Linear Shallow Term Rewrite Systems
Godoy Balil, Guillermo; Ashish, Tiwari; Rakesh, M Verma
Lecture notes in computer science
Date of publication: 200303
Journal article
Share Reference managers 
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
Presentation of work at congresses
View Share Reference managers 
Automated Deduction with Builtin Theories. Completeness Results and Constraint Solving Techniques.
Godoy Balil, Guillermo
Defense's date: 20011011
Department of Software, Universitat Politècnica de Catalunya
Theses
Share Reference managers 
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)
Presentation of work at congresses
Share Reference managers 
On Ordering Constraints For Deduction with BuiltIn Abelian Semigroups, Monoids and Groups
Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
16th Annual IEEE Symposium on Logic in Computer Science (LICS)
Presentation of work at congresses
Share Reference managers 
On the Completeness of Arbitrary Selection Strategies for Paramodulation
Bofill, M; Godoy Balil, Guillermo
Lecture notes in computer science
Date of publication: 200107
Journal article
Share Reference managers 
Modular Redundancy for Theorem Proving
Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
Int. Conf. on Frontiers of Combining Systems
Presentation of work at congresses
Share Reference managers 
Paramodulation with Builtin Abelian Groups
Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario
15th Annual IEEE Symposium on Logic nin Computer Science (LICS)
Presentation of work at congresses
Share Reference managers 
Modular Redundancy for Theorem Proving
Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
Lecture notes in computer science
Date of publication: 200003
Journal article
Share Reference managers 
Maximal Strategies for Paramodulation with NonMonotonic Orderings
Godoy Balil, Guillermo
Date: 199907
Report
Share Reference managers 
Paramodulation with nonMonotonic Orderings
Bofill, M; Godoy Balil, Guillermo; Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto
Fourteenth annual IEEE Symposium on Logic in Computer Science
Presentation of work at congresses
Share Reference managers
Filter results
UPC network collaboration
Reference managers
Continue