Reports de recerca
Recent Submissions

Firstorder completion with ordering constraints: some positive and some negative results
(19911015)
External research report
Open AccessWe show by means of counter examples that some wellknown 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
(19911015)
External research report
Open AccessWe 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 selfreducible sets
(199101)
External research report
Open AccessWe study one worddecreasing selfreducible sets, which were introduced by Lozano and Torán. These are usual selfreducible sets with the peculiarity that the selfreducibility machine makes at most one query and this is ... 
Classes of term rewrite systems with polynomial confluence problems
(20020606)
External research report
Open AccessThe confluence property of ground (i.e., variablefree) term rewrite systems (GTRS) is wellknown to be decidable. This was proved independently in [DTHL87,DHLT90] and in [Oya87] using tree automata techniques and ground ... 
The Widthsize method for general resolution is optimal
(199902)
External research report
Open AccessThe WidthSize Method for resolution was recently introduced by BenSasson and Wigderson (BSW): Short Proofs are Narrow  Resolution Made Simple STOC 99). They found a tradeoff between two complexity measures for ... 
Succinct circuit representations and leaf languages are basically the same concept
(199601)
External research report
Open AccessThis 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
(199801)
External research report
Open AccessWe 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
(199610)
External research report
Open AccessOur work concerns Frege systems, substitution Frege systems (sF), renaming Frege systems, top/bottomFrege 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
(20030601)
External research report
Open AccessThe purpose of this document is to provide an indepth 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
(199510)
External research report
Open AccessIn this work we provide a new proof of the result by Gallier and Tannen that the combination of an arbitrary terminating firstorder rewrite system with the simply typed lambda calculus is strongly normalizing. This proof ... 
Extension orderings
(199510)
External research report
Open AccessIn 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
(199506)
External research report
Open AccessWe 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 ...