Enviaments recents

  • Efficient deduction in equality Horn logic by Horn-completion 

    Nieuwenhuis, Robert Lukas Mario; Nivela Alós, M. Pilar Brígida (1991)
    Report de recerca
    Accés obert
    We present a new unfailing completion procedure for Horn clauses with equality, including goal clauses. It is refutationally complete, and improves previous methods in that superpositions are computed only with unconditional ...
  • An implementation of the KNS ordering 

    Rivero Almeida, José Miguel (1991-04)
    Report de recerca
    Accés obert
    We describe an implementation of the KNS ordering within the TRIP system, a Quintus-Prolog written laboratory for experimenting with new rewrite-like approaches to theorem proving in first-order logic. The aim of the TRIP ...
  • Automatic generation of polynomial loop invariants for imperative programs 

    Rodríguez Carbonell, Enric; Kapur, Deepak (2003-11)
    Report de recerca
    Accés obert
    A general framework is presented for automatig the discovery of loop invariants for imperative programs. Theoretical results about the correctness and completeness of the proposed method are given. More importantly, it is ...
  • First-order completion with ordering constraints: some positive and some negative results 

    Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
    Report de recerca
    Accés obert
    We show by means of counter examples that some well-known results on the completeness of deduction methods with ordering constraints are incorrect. The problem is caused by the fact that the usual lifting lemmata do not ...
  • Basic superposition is complete 

    Nieuwenhuis, Robert Lukas Mario; Rubio Gimeno, Alberto (1991-10-15)
    Report de recerca
    Accés obert
    We define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous ...
  • On one query self-reducible sets 

    Lozano Boixadors, Antoni; Ogiwara, Mitsunori (1991-01)
    Report de recerca
    Accés obert
    We study one word-decreasing self-reducible sets, which were introduced by Lozano and Torán. These are usual self-reducible sets with the peculiarity that the self-reducibility machine makes at most one query and this is ...
  • 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 Boixadors, 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 Boixadors, 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 ...

Mostra'n més