Checking Sufficient Completeness by Inductive Theorem Proving

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

Abstract

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
PublisherSpringer
Pages171-190
Number of pages20
ISBN (Print)9783031124402
DOIs
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

Conference

Conference14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/TerritoryGermany
CityMunich
Period4/2/224/3/22

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

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

Cite this