Inclusional Theories in Declarative Programming

When studying specific deduction techniques and strategies for operational semantics of logic programming languages special emphasis was put on the equality relation, due to its interest in a variety of different domains. But recently special emphasis has been put on partial order relations, and specifically on inclusions, as a basis for several different specification frameworks. It is therefore attractive to work towards a logic programming language which deals efficiently with inclusions, and which may be useful as a rapid prototyping tool. Term rewriting appears to be a suitable technique for theorem proving with inclusional theories, since it naturally applies to arbitrary (possibly non-symmetric) transitive relations, but turns out to be impractical in general. Therefore several restrictions need to be put on inclusional theories in order to improve the inference mechanism and to define efficient deduction strategies, which could be used in an operational semantics of an inclusio..