To refer to this page use:
|Abstract:||In this paper we introduce a new approach for proving quantified theorems over inductively defined data-types. We present an automated prover that searches for a sequence of simplifications and transformations to prove the validity of a given theorem, and in the absence of required lemmas, attempts to synthesize supporting lemmas based on terms and expressions witnessed during the search for a proof. The search for lemma candidates is guided by a user-specified template, along with many automated filtering mechanisms. Validity of generated lemmas is checked recursively by our prover, supported by an off-the-shelf SMT solver. We have implemented our prover called AdtInd and show that it is able to solve many problems on which a state-of-the-art prover fails.|
|Citation:||Yang, Weikun, Grigory Fedyukovich, and Aarti Gupta. "Lemma Synthesis for Automating Induction over Algebraic Data Types." In International Conference on Principles and Practice of Constraint Programming, pp. 600-617. doi:10.1007/978-3-030-30048-7_35|
|Pages:||600 - 617|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Conference on Principles and Practice of Constraint Programming|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.