# Re: [racket-users] Trying to prove a property of a semantics for logic (Prolog-like) programs: could Redex help?

```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