Reports de recerca
Recent Submissions
-
Efficient deduction in equality Horn logic by Horn-completion
(1991)
Research report
Open AccessWe 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
(1991-04)
Research report
Open AccessWe 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
(2003-11)
Research report
Open AccessA 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
(1991-10-15)
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)
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)
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)
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)
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)
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)
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)
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)
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 ...
RSS 1.0