Possible collaboration with Industry

[lyhlbyl]

https://github.com/klar42/railground

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]

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