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

Joe Hendrix, Jose Meseguer, Hitoshi Ohsaki

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationAutomated Reasoning - Third International Joint Conference, IJCAR 2006, Proceedings
PublisherSpringer-Verlag
Pages151-155
Number of pages5
ISBN (Print)3540371877, 9783540371878
StatePublished - Jan 1 2006
EventThird International Joint Conference on Automated Reasoning, IJCAR 2006 - Seattle, WA, United States
Duration: Aug 17 2006Aug 20 2006

Publication series

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

Other

OtherThird International Joint Conference on Automated Reasoning, IJCAR 2006
CountryUnited States
CitySeattle, WA
Period8/17/068/20/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A sufficient completeness checker for linear order-sorted specifications modulo axioms'. Together they form a unique fingerprint.

Cite this