Decision procedures for proving inductive theorems without induction

Takahito Aoto, Sorin Stratulat

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

6 Citations (Scopus)

Abstract

Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive reasoning. We give procedures for deciding the inductive validity of equations in some standard TRSs on natural numbers and lists. Contrary to previous decidability results, our procedures can automatically decide without involving induction reasoning the inductive validity of arbitrary equations for these TRSs, that is, without imposing any syntactical restrictions on the form of equations. We also report on the complexity of our decision procedures. These decision procedures are implemented in our automated provers for inductive theorems of TRSs and experiments are reported.

Original languageEnglish
Title of host publicationPPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
PublisherAssociation for Computing Machinery, Inc
Pages237-248
Number of pages12
ISBN (Electronic)9781450329477
DOIs
Publication statusPublished - 2014 Sep 8
Event16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014 - Canterburry, United Kingdom
Duration: 2014 Sep 82014 Sep 10

Publication series

NamePPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming

Other

Other16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014
CountryUnited Kingdom
CityCanterburry
Period14/9/814/9/10

Keywords

  • Decision procedure
  • Inductive theorems
  • Initial algebra
  • Term rewriting systems

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Decision procedures for proving inductive theorems without induction'. Together they form a unique fingerprint.

Cite this