From: Ben Hocking <benjaminhocking@gmail.com>
Subject: Mechanisms for proving rules in .rlu files
Date: Fri, 17 Aug 2012 13:39:47 -0700 (PDT)
Date: 2012-08-17T13:39:47-07:00 [thread overview]
Message-ID: <4365f56f-d4d3-440b-87bb-5cfe868608f5@googlegroups.com> (raw)
I've created a fairly large .rlu file, and I'm newly aware of the "sparkrules" tool, but I haven't found a way to prove the validity of the rules in my .rlu file. For now, I've written a converter that converts the .rlu file to a PVS theory and I'm working on proving the rules there, but this converter makes a few assumptions that are valid for my rules (all variables are integers or booleans, I'm only using a may_be_replaced_by and may_be_deduced_from, etc.) and of course might have flaws in it that I haven't detected yet.
What mechanisms do others use for proving user-defined rules?
-Ben
next reply other threads:[~2012-08-20 19:41 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-08-17 20:39 Ben Hocking [this message]
2012-08-17 21:37 ` Mechanisms for proving rules in .rlu files Alexander Senier
2012-08-19 16:33 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox