Search ACM DL

Search Issue

enter search term and/or author name

**Domain-dependent knowledge in answer set planning**

Tran Cao Son, Chitta Baral, Nam Tran, Sheila Mcilraith

Pages: 613-657

DOI: 10.1145/1183278.1183279

In this article we consider three different kinds of domain-dependent control knowledge (temporal, procedural and HTN-based) that are useful in planning. Our approach is declarative and relies on the language of logic programming with answer set...

**Defining functions on equivalence classes**

Lawrence C. Paulson

Pages: 658-675

DOI: 10.1145/1183278.1183280

A *quotient construction* defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are *equivalence...
*

*
Extensional equivalence and singleton types
Christopher A. Stone, Robert Harper
Pages: 676-722
DOI: 10.1145/1183278.1183281
We study the &lamda;^{ΠΣS}_{≤} calculus, which contains singleton types S(M) classifying terms of base type provably equivalent to the term M. The system includes dependent types for pairs and...
*

*
Efficient solving of quantified inequality constraints over the real numbers
Stefan Ratschan
Pages: 723-748
DOI: 10.1145/1183278.1183282
Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are ≤ and <. Solving such constraints is an undecidable problem...
*

*
The strength of replacement in weak arithmetic
Stephen Cook, Neil Thapen
Pages: 749-764
DOI: 10.1145/1183278.1183283
The replacement (or collection or choice) axiom scheme BB(Γ) asserts bounded quantifier exchange as follows: ∀i < |a| ∃x < aφ(i,x) →...
*

*
Splitting an operator: Algebraic modularity results for logics with fixpoint semantics
Joost Vennekens, David Gilis, Marc Denecker
Pages: 765-797
DOI: 10.1145/1183278.1183284
It is well known that, under certain conditions, it is possible to split logic programs under stable model semantics, that is, to divide such a program into a number of different “levels”, such that the models of the entire program...
*

*
Kleene algebra with domain
Jules Desharnais, Bernhard Möller, Georg Struth
Pages: 798-833
DOI: 10.1145/1183278.1183285
We propose Kleene algebra with domain (KAD), an extension of Kleene algebra by simple equational axioms for a domain and a codomain operation. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and...
*