[Why3-club] from equations to rewriting
coa at dcc.fc.up.pt
Mon Mar 17 23:56:33 CET 2014
That might do it for me.
I am looking for two things. The first is make a translation of a FO
logic formula like Conjunctive Normal Form, which can be performed by a
function in the logic.
The formulas have an evaluating function which will require some proof work
for each formula one gives it. These proofs could be easier/faster in
automatic provers if they use some equations, but in the wrong order the
equations make the structure bigger. I can always use an interactive prover
and explicitly point the equation when using it, but automatic provers save
a lot of work.
On Mon, Mar 17, 2014 at 7:33 PM, Claude Marche <Claude.Marche at inria.fr>wrote:
> A function defined by pattern-matching could be what you are looking for.
> Could you explain in more details, may be with an example, what you would
> like to do?
> - Claude
> On 03/17/2014 06:52 PM, Cláudio Amaral wrote:
>> Hello all
>> I would like to know if there is a way to specify the desired
>> directionality of an equation to define the rules wanted as in a
>> rewriting system.
>> What is supposed to be rewritten are data structures (kind of suntax
>> Why3-club mailing list
>> Why3-club at lists.gforge.inria.fr
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club