TY - GEN
T1 - Lemma Synthesis for Automating Induction over Algebraic Data Types
AU - Yang, Weikun
AU - Fedyukovich, Grigory
AU - Gupta, Aarti
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85075734083&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85075734083&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-30048-7_35
DO - 10.1007/978-3-030-30048-7_35
M3 - Conference contribution
AN - SCOPUS:85075734083
SN - 9783030300470
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 600
EP - 617
BT - Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, Proceedings
A2 - Schiex, Thomas
A2 - de Givry, Simon
PB - Springer
T2 - 25th International Conference on Principles and Practice of Constraint Programming, CP 2019
Y2 - 30 September 2019 through 4 October 2019
ER -