Reports de recerca
Enviaments recents
-
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 ... -
Lambda extensions of rewrite orderings
(1995-10)
Report de recerca
Accés obertIn 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)
Report de recerca
Accés obertIn 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)
Report de recerca
Accés obertWe 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 ... -
A Characterization of PF^NP| = PF^NP[log]
(1993-02)
Report de recerca
Accés obertSome implications of the fact PF^NP| = PF^NP[log] are known in terms of equalities between complexity classes of sets, but a characterization in the same terms is still unknown. Here we provide a characterization in terms ... -
Maximal strategies for paramodulation with non-monotonic orderings
(1999-07)
Report de recerca
Accés obertA west ordering is a well-founded (strict partial) ordering on terms that satisfies the subterm property. In [Bofill, Godoy, Nieuwenhuis, Rubio, (BGNR-LICS99)] the completeness of an ordered paramodulation inference ... -
A Fully syntactic AC-RPO
(1998-02-01)
Report de recerca
Accés obertWe present the first fully syntactic (i.e., non-interpretation-based) AC-compatible recursive path ordering (RPO). It is very simple, and hence easy to implement, and its behaviour is intuitive as in the standard RPO. ...
RSS 1.0