Skip to Main content Skip to Navigation
Book sections

Superposition with Structural Induction

Simon Cruanes 1, 2
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
2 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Superposition-based provers have been successfully used to discharge proof obligations stemming from proof assistants. However, many such obligations require induction to be proved. We present a new extension of typed superposition that can perform structural induction. Several inductive goals can be attempted within a single saturation loop, by leveraging AVATAR [1]. Lemmas obtained by generalization or theory exploration can be introduced during search, used, and proved, all in the same search space. We describe an implementation and present some promising results.
Complete list of metadata

Cited literature [39 references]  Display  Hide  Download
Contributor : Simon Cruanes Connect in order to contact the contributor
Submitted on : Friday, March 8, 2019 - 8:15:01 PM
Last modification on : Wednesday, November 3, 2021 - 7:08:53 AM
Long-term archiving on: : Monday, June 10, 2019 - 12:20:59 PM


Files produced by the author(s)




Simon Cruanes. Superposition with Structural Induction. Clare Dixon; Marcelo Finger. Frontiers of Combining Systems, Springer, pp.172-188, 2017, 11th International Symposium on Frontiers of Combining Systems - FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings, 978-3-319-66166-7. ⟨10.1007/978-3-319-66167-4_10⟩. ⟨hal-02062459⟩



Les métriques sont temporairement indisponibles