Graphic summary
  • Show / hide key
  • Information


Scientific and technological production
  •  

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

     Creus Lopez, Carles; Godoy Balil, Guillermo; Ramos Garrido, Lander
    Information processing letters
    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

  • Variants of unification considering compression and context variables

     Gascon Caro, Adrian
    Defense's date: 2014-05-30
    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.

  • 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
    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.

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

     Creus Lopez, Carles; Gascon Caro, Adrian; Godoy Balil, Guillermo
    Journal of automated reasoning
    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
    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.

  • The HOM problem is EXPTIME-complete

     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 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.

  • Unification and matching on compressed terms

     Gascon Caro, Adrian; Godoy Balil, Guillermo; Schmidt-Schauß, Manfred
    ACM transactions on computational logic
    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
    Date of publication: 2011
    Journal article

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

  • Sweetlogics-UPC

     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

  • 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
    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

  • 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
    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
    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
    Date of publication: 2010-03
    Journal article

    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
    Presentation's date: 2010
    Presentation of work at congresses

    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
    Presentation's date: 2010
    Presentation of work at congresses

    View View Open in new window  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
    Date of publication: 2009-04
    Journal article

     Share Reference managers Reference managers Open in new window

  • Undecidable properties of flat term rewrite systems

     Godoy Balil, Guillermo; Hernandez Pibernat, Hugo
    Applicable algebra in engineering communication and computing
    Date of publication: 2009-01
    Journal article

     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
    Participation in a competitive project

     Share

  • Termination of Rewriting with Right-Flat 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 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
    Participation in a 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
    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
    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
    Defense's date: 2007-05-23
    Department of Software, 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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    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
    Presentation of work at congresses

    View View Open in new window  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
    Date of publication: 2001-07
    Journal article

     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)
    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)
    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
    Defense's date: 2001-10-11
    Department of Software, Universitat Politècnica de Catalunya
    Theses

     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
    Date of publication: 2000-03
    Journal article

     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)
    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
    Int. Conf. on Frontiers of Combining Systems
    Presentation of work at congresses

     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
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window