Now showing items 1-15 of 15

    • Automated deduction with built-in theories: completeness results and constraint solving techniques 

      Godoy Balil, Guillem (Universitat Politècnica de Catalunya, 2001-10-11)
      Doctoral thesis
      Open Access
    • Automatic evaluation of context-free grammars (system description) 

      Creus López, Carles; Godoy Balil, Guillem (Springer, 2014)
      Conference report
      Restricted access - publisher's policy
      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 ...
    • Automatic evaluation of reductions between NP-complete problems 

      Creus López, Carles; Fernández Durán, Pau; Godoy Balil, Guillem (Springer, 2014)
      Conference report
      Restricted access - publisher's policy
      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 ...
    • Classes of term rewrite systems with polynomial confluence problems 

      Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario (2002-06-06)
      External research report
      Open Access
      The confluence property of ground (i.e., variable-free) term rewrite systems (GTRS) is well-known to be decidable. This was proved independently in [DTHL87,DHLT90] and in [Oya87] using tree automata techniques and ground ...
    • Decidable classes of tree automata mixing local and global constraints modulo flat theories 

      Barguño, Luis; Creus López, Carles; Godoy Balil, Guillem; Jacquemard, Florent; Vacher, Camile (2013-02)
      Article
      Open Access
      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. ...
    • Emptiness and finiteness for tree automata with global reflexive disequality constraints 

      Creus López, Carles; Gascón Caro, Adrià; Godoy Balil, Guillem (2013-12-01)
      Article
      Restricted access - publisher's policy
      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 ...
    • Excessively duplicating patterns represent non-regular languages 

      Creus López, Carles; Godoy Balil, Guillem; Ramos Garrido, Lander (2014-03-01)
      Article
      Restricted access - publisher's policy
      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 ...
    • FONAMENTS INFORMATICS (Examen 1r Quadr.) 

      Godoy Balil, Guillem (Universitat Politècnica de Catalunya, 2004-01-09)
      Exam
      Restricted access to the UPC academic community
    • Learning theory through videos: a teaching experience in a theoretical course based on self-learning videos and problem-solving sessions 

      Arias Vicente, Marta; Creus López, Carles; Gascón Caro, Adrià; Godoy Balil, Guillem (SciTePress, 2011)
      Conference report
      Restricted access - publisher's policy
      In this paper we describe a teaching experience applied to a theoretical course tought in a computer science degree. The main feature of our experiment is the introduction of videos specifically designed for self-learning ...
    • Maximal strategies for paramodulation with non-monotonic orderings 

      Bofill Arasa, Miquel; Godoy Balil, Guillem (1999-07)
      External research report
      Open Access
      A west ordering is a well-founded (strict partial) ordering on terms that satisfies the subterm property. In [Bofill, Godoy, Nieuwenhuis, Rubio, (BGNR-LICS99)] the completeness of an ordered paramodulation inference ...
    • Non-linear rewrite closure and weak normalization 

      Creus López, Carles; Godoy Balil, Guillem; Massanes Basi, Francesc d'Assis; Tiwari, Ashish Kumar (2013-10)
      Article
      Restricted access - publisher's policy
      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 ...
    • The HOM problem is EXPTIME-complete 

      Creus López, Carles; Gascon Caro, Adrian; Godoy Balil, Guillem; Ramos Garrido, Lander (2016)
      Article
      Open Access
      We define a new class of tree automata with constraints and prove decidability of the emptiness problem for this class in exponential time. As a consequence, we obtain several EXPTIME-completeness results for problems on ...
    • The HOM problem is EXPTIME-complete 

      Creus López, Carles; Gascón Caro, Adrià; Godoy Balil, Guillem; Ramos, Lander (2012)
      Conference report
      Restricted access - publisher's policy
      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. ...
    • Tree automata with height constraints between brothers 

      Creus López, Carles; Godoy Balil, Guillem (Springer, 2014)
      Conference report
      Restricted access - publisher's policy
      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. ...
    • Unification and matching on compressed terms 

      Gascón Caro, Adrià; Godoy Balil, Guillem; Schmidt-Schauß, Manfred (2011-07-29)
      Article
      Restricted access - publisher's policy
      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 ...