Reports de recerca
Enviaments recents
-
Efficient deduction in equality Horn logic by Horn-completion
(1991)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertA 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)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertThe 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)
Report de recerca
Accés obertThe 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)
Report de recerca
Accés obertThis 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)
Report de recerca
Accés obertWe 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)
Report de recerca
Accés obertOur 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)
Report de recerca
Accés obertThe 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 ...