Now showing items 1-11 of 11

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