You may also wish to look into Rosette, a Racket-based SMT DSL. Emina Torlak is the creator and you should be able to find it from her web site — Matthias
> On Dec 5, 2017, at 1:37 AM, Vincent Nys <vincent...@gmail.com> wrote: > > Matthias, > > Thank you for your input. I will look into enlisting a proof assistant. > > Regards, > > Vincent > > Op maandag 4 december 2017 19:23:16 UTC+1 schreef Matthias Felleisen: > > > On Dec 4, 2017, at 9:47 AM, Vincent Nys <vince...@ <>gmail.com > > <http://gmail.com/>> wrote: > > > > 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? > > > Let me first clarify a misunderstanding. Redex is not really a tool for > writing an interpreter. If you want to write interpreters, use Racket or > Typed Racket. Redex is a tool for specifying either a reduction semantics or > a relation semantics. It’s unique for the former and one among others for the > latter. > > Let me then state a surprising admission. Even though I started as a Prologer > and have always thought of reduction semantics as a unique and amazing tool > for specifying a semantics, I have never done so for a logic language. > Interesting. > > Now as to your question, Redex can check things but it’s hard to prove them, > even for finite cases. In the past some of my PhD students have developed > Redex model to experiment with a semantics and Isabelle/Coq proofs to prove > things. Modeling in Redex tends to be fast and easy; it really feels like it > imposes only a slightly higher overhead than paper-and-pencil modeling. > > Many wish that proof systems and Redex were more integrated. Alas they are > not. > > — Matthias > > > -- > 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 > <mailto:racket-users+unsubscr...@googlegroups.com>. > For more options, visit https://groups.google.com/d/optout > <https://groups.google.com/d/optout>. -- 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.
