Constraint Theory

Abduction is the ability to reason from observed results to the basic missing facts from which they follow. In artificial intelligence, abduction has been embraced to overcome limitations of deductive reasoning. I have applied constraint abduction to the inference problem for GADTs and EADTs. In [17], I co-designed an extension of the CHR solving mechanism which incorporates abductive reasoning to solve implication constraints.

Confluence is a critical property for any ``rewrite'' based language. A particularly interesting example are CHRs which define rewritings from one multiset of constraints to another. For terminating CHRs there is a decidable test for confluence. But many CHR programs that in practice are confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not reachable in practice. In [6], I co-designed a new notion of observable confluence, a weaker notion of confluence which takes into account whether states are observable. For an important class of non-confluent programs arising from Haskell type class programs with functional dependencies, it can be shown that they are observable confluent.

Martin Sulzmann 2006-07-19