Hi, 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, Vincent -- 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 to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
