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

Reply via email to