enter search term and/or author name
Automatic generation of rule-based constraint solvers over finite domains
Slim Abdennadher, Christophe Rigotti
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
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
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
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
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
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  using tree automata techniques and ground tree...
Some applications of logic to feasibility in higher types
Aleksandar Ignjatovic, Arun Sharma
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
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...