Modal/higher order logic

[Robert Goldman]

This is a follow-up to the case-based reasoning question I asked earlier :

One way to do this modal-style or higher order reasoning would be to use HiLog (iiuc). But this seems to push one into writing a meta-interpreter, something like the following:

case(?case)(?P) :- isbasefact{P@?case} ; isbasefact{P@main}.

case(?case)(?P) :- clause{?P@?case, ?Q}, case(?case)(?Q). case(?case)(?P) :- clause{?P@main, ?Q}, case(?case)(?Q). case(?case)((?G1, ?G2)) :- case(?case)(?G1), case(?case)(?G2).

case(?case)((?G1 ; ?G2)) :- case(?case)(?G1) ; case(?case)(?G2).

...and so on...

It seems to me that, compared to Prolog, Ergo's syntax has so many features (if-then-else, etc.) that it would be quite difficult to write a meta-interpreter for it. Is that correct? Or am I missing something?  Is there some more restricted recursion that could be used?

Even if one limits oneself to cases being a collection of base facts, one still needs to have recursive rules for clauses, like the above, to distribute the case modality over the internals of a rule.

\Box (A and B) \equiv \Box A and \Box B.

Thank you for any suggestions