Display program code

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: 

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