| Tom Schrijvers 2006-02-08, 7:02 pm |
| Benjamin Johnston wrote:
> Hi,
>
> I've been playing around with CHR (in SWI-Prolog) lately. I think I'm
> fairly comfortable with what appears to be the "standard" usage of CHR,
> but in a recent project I needed a propositional theorem prover.
>
> Thom Fruhwirth, in slides from his talk "CHR around the world" outlines
> a theorem prover implemented in CHR using resolution. It struck me,
> however, that it might also be able to implement it using analytical
> tableaux. I came up with this (operators have been defined):
>
> satisfiable(not (X and Y)) <=> satisfiable(not X or not Y).
> satisfiable(X and Y) <=> satisfiable(X), satisfiable(Y).
> satisfiable(not (X or Y)) <=> satisfiable(not X and not Y).
> satisfiable(not not X) <=> satisfiable(X).
> satisfiable(X or Y) <=> satisfiable(X) ; satisfiable(Y).
> satisfiable(not X), satisfiable(X) <=> fail.
> satisfiable(X) \ satisfiable(X) <=> true.
>
> tautology(Stmt) :-
> \+ satisfiable(not Stmt).
>
> The interesting line is the rule for (X or Y), appearing 3rd from the
> bottom. This makes the system non-confluent (according to Thom's
> definition), and seems to go against the spirit of most tutorials on
> CHR -- for starters, it means adding a constraint results in a
> choice-point.
>
> But, the thing is that it works; and I think it looks quite nice too.
> It could probably be rewritten so that it explicitly represents each
> "choice point", but then it wouldn't be quite so elegant.
>
>
> So, what I would like to know is if there is any established
> "CHR-style". Does this make you more experienced CHR users recoil in
> horror at the abuse... or is this just a "cute hack"... or even
> legitimate code in line with your expected use of CHR?
There is no shame in having a disjunction in the body of a rule. It is
quite accepted in the CHR world. In fact, CHR extended with disjunctions
in the bodies of rules is called CHR^\vee and several papers exist that
refer to it. The most important ones are probably:
Constraint handling rules with disjunction
S. Abdennadher, Research report PMS-FB-1999-5, Computer Science
Department, ..., 1999
and
Essentials of Constraint Programming
Thom Frühwirth and Slim Abdennadher, Textbook, Springer Verlag, 2003.
But even last year's CHR workshop had a paper about optimized
compilation of CHR^\vee programs:
A High Performance CHRv Execution Engine.
Luis Menezes, Jairson Vitorino, Marcos Aurelio, CHR 2005
I think your issue with disjunction comes from the fact that search is
(considered) less efficient in the constraint programming world than
dealing with all cases at once ('lifting' the disjunction in the
constraints). From a logical point of view both would be equivalent.
That aside, I agree with Bart: practical CHR-style programs use whatever
the host language has to offer. Personally, I would encourage you very
much to experiment with combinations of features and see what suits you
best, what gives you more expressive power. Use the best of both worlds.
Cheers,
Tom
|