Checking Sufficient Completeness by Inductive Theorem Proving

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


Sufficient completeness of an equational program ensures that each input can be fully evaluated to a data result. Checking this fundamental property for programs in expressive equational languages supporting conditional equations, types and subtypes, and rewriting modulo structural axioms is a challenging problem for which few methods currently exist. This work presents a new method that reduces sufficient completeness verification to a standard inductive theorem proving problem for a wide class of conditional equational programs in such languages.

Original languageEnglish (US)
Title of host publicationRewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
EditorsKyungmin Bae
Number of pages20
ISBN (Print)9783031124402
StatePublished - 2022
Event14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany
Duration: Apr 2 2022Apr 3 2022

Publication series

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


Conference14th International Workshop on Rewriting Logic and its Applications, WRLA 2022

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Checking Sufficient Completeness by Inductive Theorem Proving'. Together they form a unique fingerprint.

Cite this