Reports de recerca
Recent Submissions
-
First-order completion with ordering constraints: some positive and some negative results
(1991-10-15)
External research report
Open AccessWe 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
(1991-10-15)
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 self-reducible sets
(1991-01)
External research report
Open AccessWe 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
(2002-06-06)
External research report
Open AccessThe 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
(1999-02)
External research report
Open AccessThe 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
(1996-01)
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
(1998-01)
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
(1996-10)
External research report
Open AccessOur 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
(2003-06-01)
External research report
Open AccessThe 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
(1995-10)
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 first-order rewrite system with the simply typed lambda calculus is strongly normalizing. This proof ... -
Extension orderings
(1995-10)
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
(1995-06)
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 ...
RSS 1.0