Possible collaboration with Industry

ggrov / tinker

Graph based proof strategy language

http://ggrov.github.io/tinker/

6 stars 0 forks source link

Open lyhlbyl opened 8 years ago

lyhlbyl commented 8 years ago

from abz2016

[ ] logging + PSGraph as proof report
[ ] using gt as a guide to find a possible applicable tactic from library (proof hints)

short term

[ ] encode the tactic and gt required in the case studies long term
[ ] generic solution to provide interface to allow users to provide definitions
[ ] use of ripping and critics in the rail case (Yuhui's thesis) see dev/rail for more details

lyhlbyl commented 8 years ago

1) from existing Rodin proof -> PSGraph 2) validate that two PSGraph are semantically the same