Hello,
I'm trying to learn hol, and one thing is not clear to me is how to mix
forward proof in a goal directed proof while being in an active goal
package session.
One thing I was trying is to complete a proof with this current goalstack:
?v. R (t',v) /\ R (u,v)
------------------------------------
0. !u. R (t,u) ==> ?v. R (t,v) /\ R (u,v)
1. R (t',u)
How can I apply GEN to the assumption 0 and then MP on the new 0 and 1?
Thanks for any suggestion.
Kind Regards,
Domenico
------------------------------------------------------------------------------
October Webinars: Code for Performance
Free Intel webinars can help you accelerate application performance.
Explore tips for MPI, OpenMP, advanced profiling, and more. Get the most from
the latest Intel processors and coprocessors. See abstracts and register >
http://pubads.g.doubleclick.net/gampad/clk?id=60135031&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
