Lemma Synthesis for Automating Induction over Algebraic Data Types

Weikun Yang, Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationPrinciples and Practice of Constraint Programming - 25th International Conference, CP 2019, Proceedings
EditorsThomas Schiex, Simon de Givry
PublisherSpringer
Pages600-617
Number of pages18
ISBN (Print)9783030300470
DOIs
StatePublished - Jan 1 2019
Event25th International Conference on Principles and Practice of Constraint Programming, CP 2019 - Stamford , United States
Duration: Sep 30 2019Oct 4 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11802 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Principles and Practice of Constraint Programming, CP 2019
CountryUnited States
CityStamford
Period9/30/1910/4/19

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Lemma Synthesis for Automating Induction over Algebraic Data Types'. Together they form a unique fingerprint.

Cite this