Computational Logic (TOCL)


Search Issue
enter search term and/or author name


ACM Transactions on Computational Logic (TOCL), Volume 7 Issue 4, October 2006

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