| HAL-Inria | Publications, software ... of Inria's scientists |
Book sections
Superposition with Structural Induction
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.
Cited literature [39 references]
https://hal.inria.fr/hal-02062459
Contributor : Simon Cruanes <>
Submitted on : Friday, March 8, 2019 - 8:15:01 PM
Last modification on : Wednesday, April 3, 2019 - 1:23:16 AM
Document(s) archivé(s) le : Monday, June 10, 2019 - 12:20:59 PM
Contributor : Simon Cruanes <>
Submitted on : Friday, March 8, 2019 - 8:15:01 PM
Last modification on : Wednesday, April 3, 2019 - 1:23:16 AM
Document(s) archivé(s) le : Monday, June 10, 2019 - 12:20:59 PM
File
frocos_17_paper.pdf
Files produced by the author(s)