Enviaments recents

  • Classes of term rewrite systems with polynomial confluence problems 

    Godoy Balil, Guillem; Nieuwenhuis, Robert Lukas Mario (2002-06-06)
    Report de recerca
    Accés obert
    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 ...
  • The Width-size method for general resolution is optimal 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1999-02)
    Report de recerca
    Accés obert
    The Width-Size Method for resolution was recently introduced by Ben-Sasson and Wigderson (BSW): Short Proofs are Narrow - Resolution Made Simple STOC 99). They found a trade-off between two complexity measures for ...
  • Succinct circuit representations and leaf languages are basically the same concept 

    Borchert, Bernd; Lozano Bojados, Antoni (1996-01)
    Report de recerca
    Accés obert
    This paper connects two topics of Complexity Theory: The topic of succinct circuit representations initiated by Galperin and Wigderson, and the topic of leaf languages. A Boolean circuit c describes in a natural way the ...
  • On the complexity of moving vertices in a graph 

    Lozano Bojados, Antoni; Raghavan, Vijay (1998-01)
    Report de recerca
    Accés obert
    We consider the problem of deciding whether a given graph G has an automorphism which moves at least k vertices (where k is a function of |V(G)|), a question originally posed by Lubiw (1981). Here we show that this ...
  • Linear lower bounds and simulations in Frege systems with substitutions 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1996-10)
    Report de recerca
    Accés obert
    Our work concerns Frege systems, substitution Frege systems (sF), renaming Frege systems, top/bottom-Frege systems and extended Frege systems (eF). Urquhart shows that tautologies associated to a binary strings ...
  • CBR and MBR techniques: review for an application in the emergencies domain 

    Merida-Campos, Carlos; Rollón Rico, Emma (2003-06-01)
    Report de recerca
    Accés obert
    The purpose of this document is to provide an in-depth analysis of current reasoning engine practice and the integration strategies of Case Based Reasoning and Model Based Reasoning that will be used in the design and ...
  • Lambda extensions of rewrite orderings 

    Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (1995-10)
    Report de recerca
    Accés obert
    In this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof ...
  • Extension orderings 

    Rubio Gimeno, Alberto (1995-10)
    Report de recerca
    Accés obert
    In this paper we study how to extend a collection of term orderings on disjoint signatures to a single one, called an extension ordering, which preserves (part of) their properties. Apart of its own interest, e.g. in ...
  • Constraint satisfaction as global optimization 

    Meseguer González, Pedro; Larrosa Bondia, Francisco Javier (1995-06)
    Report de recerca
    Accés obert
    We present an optimization formulation for discrete binary CSP, based on the construction of a continuous function A(P) whose global maximum represents the best possible solution for that problem. By the best possible ...
  • A Characterization of PF^NP| = PF^NP[log] 

    Lozano Bojados, Antoni (1993-02)
    Report de recerca
    Accés obert
    Some implications of the fact PF^NP| = PF^NP[log] are known in terms of equalities between complexity classes of sets, but a characterization in the same terms is still unknown. Here we provide a characterization in terms ...
  • Maximal strategies for paramodulation with non-monotonic orderings 

    Bofill Arasa, Miquel; Godoy Balil, Guillem (1999-07)
    Report de recerca
    Accés obert
    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 ...
  • A Fully syntactic AC-RPO 

    Rubio Gimeno, Alberto (1998-02-01)
    Report de recerca
    Accés obert
    We present the first fully syntactic (i.e., non-interpretation-based) AC-compatible recursive path ordering (RPO). It is very simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. ...

Mostra'n més