I'm currently working on a program transformation technique for logic
programs. The technique uses abstract interpretation, so I have an abstract
program semantics and the main operation is an abstraction of resolution. I
would like to prove a particular property of this semantics (namely that
the number of non-equivalent abstract conjunctions that can be obtained
through resolution is finite unless there are recursive calls which can be
characterized in a specific way). I can't seem to do it by hand. Would
Redex be of help if I used it to code an interpreter for these abstract
semantics? I don't necessarily mean that it should produce a complete
proof, but, for example, could it demonstrate that the property holds for a
logic program with at most N clauses of length L, where neither is
symbolic, by exhausting a search space?
Thanks in advance,
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
For more options, visit https://groups.google.com/d/optout.