A light-weight integration of automated and interactive theorem proving

摘要

In this paper, aimed at dependently typed programmers, we present a novel connectionrnbetween automated and interactive theorem proving paradigms. The novelty is that thernconnection offers a better trade-off between usability, efficiency and soundness whenrncompared to existing techniques. This technique allows for a powerful interactive proofrnframework that facilitates efficient verification of finite domain theorems and guidedrnconstruction of the proof of infinite domain theorems. Such situations typically occur withrnindustrial verification. As a case study, an embedding of SAT and CTL model checking isrnpresented, both of which have been implemented for the dependently typed proof assistantrnAgda.rnFinally, an example of a real world railway control system is presented, and shown using ourrnproof framework to be safe with respect to an abstract model of trains not colliding orrnderailing. We demonstrate how to formulate safety directly and show using interactiverntheorem proving that signalling principles imply safety. Therefore, a proof by an automatedrntheorem prover that the signalling principles hold for a concrete system implies the overallrnsafety. Therefore, instead of the need for domain experts to validate that the signallingrnprinciples imply safety they only need to make sure that the safety is formulated correctly.rnTherefore, some of the validation is replaced by verification using interactive theoremrnproving.