Search

Demonic composition, demonic refinement and demonic union are alternatives to the usual 'angelic' composition, angelic refinement (inclusion) and angelic (usual) union defined on binary relations. We first motivate both the angelic and the demonic via an analysis of the behaviour of non-deterministic programs, with the angelic associated with partial correctness and demonic with total correctness, both cases emerging from a richer algebraic model of non-deterministic programs incorporating both aspects. Zareckiĭ has shown that the isomorphism class of algebras of binary relations under angelic composition and inclusion is finitely axiomatized as the class of ordered semigroups. The proof can be used to establish that the same axiomatization applies to binary relations under demonic composition and refinement, and a further modification of the proof can be used to incorporate a zero element representing the empty relation in the angelic case and the full relation in the demonic case. For the signature of angelic composition and union, it is known that no finite axiomatization exists, and we show the analogous result for demonic composition and demonic union by showing that the same axiomatization holds for both. We show that the isomorphism class of algebras of binary relations with the 'mixed' signature of demonic composition and angelic inclusion has no finite axiomatization. As a contrast, we show that the isomorphism class of partial algebras of binary relations with the partial operation of constellation product and inclusion (also a 'mixed' signature) is finitely axiomatizable. [ABSTRACT FROM AUTHOR]

Abstract Binary Constraint Problems have traditionally been considered as Network Satisfaction Problems over some relation algebra. A constraint network is satisfiable if its nodes can be mapped into some representation of the relation algebra in such a way that the constraints are preserved. A qualitative representation ϕ is like an ordinary representation, but instead of requiring that (a ; b) ϕ is the composition a ϕ ∘ b ϕ of the relations a ϕ and b ϕ , as we do for ordinary representations, we only require that c ϕ ⊇ a ϕ ∘ b ϕ ⇔ c ≥ a ; b , for each c in the algebra. A constraint network is qualitatively satisfiable if its nodes can be mapped to elements of a qualitative representation, preserving the constraints. If a constraint network is satisfiable then it is clearly qualitatively satisfiable, but the converse can fail, as we show. However, for a wide range of relation algebras including the point algebra, the Allen Interval Algebra, RCC8 and many others, a network is satisfiable if and only if it is qualitatively satisfiable. Unlike ordinary composition, the weak composition arising from qualitative representations need not be associative, so we can generalise by considering network satisfaction problems over non-associative algebras. We prove that computationally, qualitative representations have many advantages over ordinary representations: whereas many finite relation algebras have only infinite representations, every finite qualitatively representable algebra has a finite qualitative representation; the representability problem for (the atom structures of) finite non-associative algebras is NP-complete ; the network satisfaction problem over a finite qualitatively representable algebra is always in NP ; the validity of equations over qualitative representations is co-NP-complete. On the other hand we prove that there is no finite axiomatisation of the class of qualitatively representable algebras. [ABSTRACT FROM AUTHOR]

Hirsch and Hodkinson proved, for 3 ≤ m < ω and any k < ω. that the class SNrmCAm+k+1 is strictly contained in SNrmCAm+k and if A k ≥ 1 then the former class cannot be defined by any finite set of first-order formulas, within the latter class. We generalize this result to the following algebras of m-ary relations for which the neat reduct operator ... is meaningful: polyadic algebras with or without equality and substitution algebras. We also generalize this result to allow the case where m is an infinite ordinal. using quasipolyadic algebras in place of polyadic algebras (with or without equality). [ABSTRACT FROM AUTHOR]

We prove that algebras of binary relations whose similarity type includes intersection, union, and one of the residuals of relation composition form a nonfinitely axiomatizable quasivariety and that the equational theory is not finitely based. We apply this result to the problem of the completeness of the positive fragment of relevance logic with respect to binary relations. [ABSTRACT FROM AUTHOR]