Checking Sufficient Completeness by Inductive Theorem Proving

José Meseguer

doi:10.1007/978-3-031-12441-9_9

Checking Sufficient Completeness by Inductive Theorem Proving

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers
Editors	Kyungmin Bae
Publisher	Springer
Pages	171-190
Number of pages	20
ISBN (Print)	9783031124402
DOIs	https://doi.org/10.1007/978-3-031-12441-9_9
State	Published - 2022
Event	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 - Munich, Germany Duration: Apr 2 2022 → Apr 3 2022

Publication series

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

Conference

Conference	14th International Workshop on Rewriting Logic and its Applications, WRLA 2022
Country/Territory	Germany
City	Munich
Period	4/2/22 → 4/3/22

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-031-12441-9_9

Library availability

Discover UIUC Full Text

Cite this

Meseguer, J. (2022). Checking Sufficient Completeness by Inductive Theorem Proving. In K. Bae (Ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers (pp. 171-190). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS). Springer. https://doi.org/10.1007/978-3-031-12441-9_9

Checking Sufficient Completeness by Inductive Theorem Proving. / Meseguer, José.

Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. ed. / Kyungmin Bae. Springer, 2022. p. 171-190 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13252 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Meseguer, J 2022, Checking Sufficient Completeness by Inductive Theorem Proving. in K Bae (ed.), Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13252 LNCS, Springer, pp. 171-190, 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022, Munich, Germany, 4/2/22. https://doi.org/10.1007/978-3-031-12441-9_9

Meseguer J. Checking Sufficient Completeness by Inductive Theorem Proving. In Bae K, editor, Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. Springer. 2022. p. 171-190. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-12441-9_9

Meseguer, José. / Checking Sufficient Completeness by Inductive Theorem Proving. Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers. editor / Kyungmin Bae. Springer, 2022. pp. 171-190 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3341d6463748423e8b66bc458b2a289a,

title = "Checking Sufficient Completeness by Inductive Theorem Proving",

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.",

author = "Jos{\'e} Meseguer",

note = "Publisher Copyright: {\textcopyright} 2022, Springer Nature Switzerland AG.; 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022 ; Conference date: 02-04-2022 Through 03-04-2022",

year = "2022",

doi = "10.1007/978-3-031-12441-9_9",

language = "English (US)",

isbn = "9783031124402",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "171--190",

editor = "Kyungmin Bae",

booktitle = "Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers",

address = "Germany",

}

TY - GEN

T1 - Checking Sufficient Completeness by Inductive Theorem Proving

AU - Meseguer, José

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85135845817&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85135845817&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-12441-9_9

DO - 10.1007/978-3-031-12441-9_9

M3 - Conference contribution

AN - SCOPUS:85135845817

SN - 9783031124402

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 171

EP - 190

BT - Rewriting Logic and Its Applications - 14th International Workshop, WRLA 2022, Revised Selected Papers

A2 - Bae, Kyungmin

PB - Springer

T2 - 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022

Y2 - 2 April 2022 through 3 April 2022

ER -