Re: [isabelle] The Incredible Proof Machine



Dear Peter,

Am Donnerstag, den 24.09.2015, 17:54 +0200 schrieb Peter Lammich:
> Just one experience when I played around with it, which puzzled me,
> and might severely puzzle your students: I tried A&B&C ==> A&C, my attempt
> is attached.
> 
> As I did not know whether & binds to left or right, I ended up 
> attaching the line to the wrong exit. But then, I got an error on the 
> line from the start, which was fine previously. I.e., when I attach 
> something to a block, I may get an error at a seemingly unrelated
> point.

Right. One of my ideas is to keep track of the order in which
connections have been added (or been changed), and apply unification in
that order. In fact, I think I forgot that I planned to do this, so I
better create an issue for it:
https://github.com/nomeata/incredible/issues/26

> Moreover, if I have something like
>   A&B&C ---> (dest-AND) 
> 
> I would like to "see" which propositions are available at the
> outputs.

You can always âpull outâ a connection (without connecting it to
something else) and see whatâs on it. But it would be more convenient
to see something right away; this is also planned:
https://github.com/nomeata/incredible/issues/24

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.