enter search term and/or author name
Domain-dependent knowledge in answer set planning
Tran Cao Son, Chitta Baral, Nam Tran, Sheila Mcilraith
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
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
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
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
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
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
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...