A sufficient completeness checker for linear order-sorted specifications modulo axioms

Joe Hendrix; José Meseguer; Hitoshi Ohsaki

doi:10.1007/11814771_14

A sufficient completeness checker for linear order-sorted specifications modulo axioms

Joe Hendrix, José Meseguer, Hitoshi Ohsaki

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

Abstract

We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.

Original language	English (US)
Title of host publication	Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings
Publisher	Springer
Pages	151-155
Number of pages	5
ISBN (Print)	3540371877, 9783540371878
DOIs	https://doi.org/10.1007/11814771_14
State	Published - 2006
Event	Third International Joint Conference on Automated Reasoning, IJCAR 2006 - Seattle, WA, United States Duration: Aug 17 2006 → Aug 20 2006

Publication series

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

Other

Other	Third International Joint Conference on Automated Reasoning, IJCAR 2006
Country/Territory	United States
City	Seattle, WA
Period	8/17/06 → 8/20/06

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/11814771_14

Library availability

Discover UIUC Full Text

Cite this

Hendrix, J., Meseguer, J., & Ohsaki, H. (2006). A sufficient completeness checker for linear order-sorted specifications modulo axioms. In Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings (pp. 151-155). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4130 LNAI). Springer. https://doi.org/10.1007/11814771_14

A sufficient completeness checker for linear order-sorted specifications modulo axioms. / Hendrix, Joe; Meseguer, José; Ohsaki, Hitoshi.
Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Springer, 2006. p. 151-155 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4130 LNAI).

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

Hendrix, J, Meseguer, J & Ohsaki, H 2006, A sufficient completeness checker for linear order-sorted specifications modulo axioms. in Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4130 LNAI, Springer, pp. 151-155, Third International Joint Conference on Automated Reasoning, IJCAR 2006, Seattle, WA, United States, 8/17/06. https://doi.org/10.1007/11814771_14

Hendrix J, Meseguer J, Ohsaki H. A sufficient completeness checker for linear order-sorted specifications modulo axioms. In Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Springer. 2006. p. 151-155. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11814771_14

Hendrix, Joe ; Meseguer, José ; Ohsaki, Hitoshi. / A sufficient completeness checker for linear order-sorted specifications modulo axioms. Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings. Springer, 2006. pp. 151-155 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{9ec4e9df9f004dc592d0b00f864a675a,

title = "A sufficient completeness checker for linear order-sorted specifications modulo axioms",

abstract = "We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.",

author = "Joe Hendrix and Jos{\'e} Meseguer and Hitoshi Ohsaki",

year = "2006",

doi = "10.1007/11814771_14",

language = "English (US)",

isbn = "3540371877",

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

publisher = "Springer",

pages = "151--155",

booktitle = "Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings",

address = "Germany",

note = "Third International Joint Conference on Automated Reasoning, IJCAR 2006 ; Conference date: 17-08-2006 Through 20-08-2006",

}

TY - GEN

T1 - A sufficient completeness checker for linear order-sorted specifications modulo axioms

AU - Hendrix, Joe

AU - Meseguer, José

AU - Ohsaki, Hitoshi

PY - 2006

Y1 - 2006

N2 - We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.

AB - We present a tool for checking the sufficient completeness of left-linear, order-sorted equational specifications modulo associativity, commutativity, and identity. Our tool treats this problem as an equational tree automata decision problem using the tree automata library CETA, which we also introduce in this paper. CETA implements a semi-algorithm for checking the emptiness of a class of tree automata that are closed under Boolean operations and an equational theory containing associativity, commutativity and identity axioms. Though sufficient completeness for this class of specifications is undecidable in general, our tool is a decision procedure for subcases known to be decidable, and has specialized techniques that are effective in practice for the general case.

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

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

U2 - 10.1007/11814771_14

DO - 10.1007/11814771_14

M3 - Conference contribution

AN - SCOPUS:33749548820

SN - 3540371877

SN - 9783540371878

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

SP - 151

EP - 155

BT - Automated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings

PB - Springer

T2 - Third International Joint Conference on Automated Reasoning, IJCAR 2006

Y2 - 17 August 2006 through 20 August 2006

ER -

A sufficient completeness checker for linear order-sorted specifications modulo axioms

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this