ACM DL

Computational Logic (TOCL)

Menu

Search Issue
enter search term and/or author name

Archive


ACM Transactions on Computational Logic (TOCL), Volume 5 Issue 2, April 2004

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...