Search ACM DL

Search Issue

enter search term and/or author name

**Automatic generation of rule-based constraint solvers over finite domains**

Slim Abdennadher, Christophe Rigotti

Pages: 177-205

DOI: 10.1145/976706.976707

A general approach to implement propagation and simplification of constraints consists of applying rules over these constraints. However, a difficulty that arises frequently when writing a constraint solver is to determine the constraint propagation...

**A logic programming approach to knowledge-state planning**: Semantics and complexity

Thomas Eiter, Wolfgang Faber, Nicola Leone, Gerald Pfeifer, Axel Polleres

Pages: 206-263

DOI: 10.1145/976706.976708

We propose a new declarative planning language, called K, which is based on principles and methods of logic programming. In this language, transitions between states of knowledge can be described, rather than transitions between completely described...

**Convergent approximate solving of first-order constraints by approximate quantifiers**

Stefan Ratschan

Pages: 264-281

DOI: 10.1145/976706.976709

Exactly solving first-order constraints (i.e., first-order formulas over a certain predefined structure) can be a very hard, or even undecidable problem. In continuous structures like the real numbers it is promising to compute approximate solutions...

**Inflationary fixed points in modal logic**

Anuj Dawar, Erich Grädel, Stephan Kreutzer

Pages: 282-315

DOI: 10.1145/976706.976710

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed-point operators have...

**Optimal length tree-like resolution refutations for 2SAT formulas**

K. Subramani

Pages: 316-320

DOI: 10.1145/976706.976711

In this article, we exploit the graphical structure of 2SAT formulas to show that the shortest tree-like resolution refutation of an unsatisfiable 2SAT formula can be determined in polynomial time.

**Classes of term rewrite systems with polynomial confluence problems**

Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari

Pages: 321-331

DOI: 10.1145/976706.976712

The confluence property of ground (i.e., variable-free) term rewrite systems (TRS) is well known to be decidable. This was proved independently in Dauchet et al. [1987, 1990] and in Oyamaguchi [1987] using tree automata techniques and ground tree...

**Some applications of logic to feasibility in higher types**

Aleksandar Ignjatovic, Arun Sharma

Pages: 332-350

DOI: 10.1145/976706.976713

While it is commonly accepted that computability on a Turing machine in polynomial time represents a correct formalization of the notion of a *feasibly computable* function, there is no similar agreement on how to extend this notion on...

**A decomposition-based implementation of search strategies**

Laurent Michel, Pascal Van Hentenryck

Pages: 351-383

DOI: 10.1145/976706.976714

Search strategies, that is, strategies that describe how to explore search trees, have raised much interest for constraint satisfaction in recent years. In particular, limited discrepancy search and its variations have been shown to achieve...