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

2017-12-05 Thread Vincent Nys
So many reasons to dig into things I've wanted to look at for a while! Op dinsdag 5 december 2017 18:23:37 UTC+1 schreef Matthias Felleisen: > > > 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 — >

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

2017-12-05 Thread Matthias Felleisen
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 wrote: > > Matthias, > > Thank you for your input. I will look into enlisting a proof assista

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

2017-12-04 Thread Vincent Nys
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 > wrote: > > > > Hi, > > > > I'm currently working on a program transform

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

2017-12-04 Thread Matthias Felleisen
> On Dec 4, 2017, at 9:47 AM, Vincent Nys 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 > wou