[Why3-club] from equations to rewriting

Cláudio Amaral 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.

/Cláudio


On Mon, Mar 17, 2014 at 7:33 PM, Claude Marche <Claude.Marche at inria.fr>wrote:

>
> Hi,
>
> 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
>> trees).
>>
>> Regards
>> Cláudio
>>
>>
>> _______________________________________________
>> Why3-club mailing list
>> Why3-club at lists.gforge.inria.fr
>> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>>
>>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140317/7a92bfd0/attachment.html>


More information about the Why3-club mailing list