Towards A New Type of Prover: On the Benefits of Discovering Sequences of "Related" Proofs

Description

This extended abstract has been written with two goals in mind: 1) to motivate the need for a prover which derives sequences of proofs rather than a single proof, and 2) to present this problem to an audience of experts who can critique this approach and who may be interested in the further development of this project. A {\em uniform sequence prover} can address issues arising in the area of inductive theorem proving, in particular automated discovery of induction invariants by instance analysis. We illustrate this approach using a novel tree grammar based method introduced by S. Eberhard and S. Hetzl (implemented as {\em Viper} within the GAPT system). This method necessitates that first-order theorem prover produces sequences of instance proofs which are ``related''. This notion of related has so far remained extra-logical and any precision has come form empirical analysis of numerous examples.

Period	08 Apr 2019
Event title	AITP
Event type	Conference
Location	AustriaShow on map