rationaltree_exist.pl : Rational tree with exist. quantifiers
CHR solver for existentially quantified conjunctions of non-flat equations overs trees with quadratic complexity.
The algorithm includes three parts:
* Transforms the original equations into equivalent existentially quantified flat equations.
* Applies the classic rationaltree solver (with term-order where existentially quantified variables are smaller than free variables).
* The reachability of variables and equations is analysed, unreachable ones are removed.

How to use:
Existentially quantified variables are identified by exists(V) where V is a list of variables. This must be the first constraint.
Equality between trees A and B is written as A eq B.
To trigger elimination of unreachable variables and equations the last constraint must be elim.
In the answer the constraints exists_s(V) and A eq_s B (for solved) are used.

Program: Change the code, then submit!

Console: Enter query or select example from below, then submit and wait for answer!

 Select example query: (Clear query) exists([X,Y,Z,V]), f(X) eq f(g(X,Y)), Z eq f(V), Z eq f(f(Y)), elim. exists([Y,Z]), f(X) eq f(g(X,Y)), Z eq f(V), Z eq f(f(Y)), elim. exists([X,Y,U]), h(Y,f(a),g(X,a)) eq h(f(U),Y,g(h(Y),U)), elim. f(X) eq X, X eq f(f(X)), elim. a eq b, elim.

WebCHR help - CHR Website - (c) Copyrights Martin Kaeser Uni Ulm 2007