Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs.
Saved in:
| Title: | Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs. |
|---|---|
| Authors: | Nakamura, Masaki1, Ogata, Kazuhiro2, Futatsugi, Kokichi2 |
| Source: | Proceedings of the International MultiConference of Engineers & Computer Scientists 2013. 2013, p1-6. 6p. |
| Subjects: | Rewriting systems (Computer science), Machine theory, Mathematical logic, Control theory (Engineering), Artificial intelligence |
| Abstract: | OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR] |
| Copyright of Proceedings of the International MultiConference of Engineers & Computer Scientists 2013 is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 96697248 AccessLevel: 6 PubType: Conference PubTypeId: conference PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Nakamura%2C+Masaki%22">Nakamura, Masaki</searchLink><relatesTo>1</relatesTo><br /><searchLink fieldCode="AR" term="%22Ogata%2C+Kazuhiro%22">Ogata, Kazuhiro</searchLink><relatesTo>2</relatesTo><br /><searchLink fieldCode="AR" term="%22Futatsugi%2C+Kokichi%22">Futatsugi, Kokichi</searchLink><relatesTo>2</relatesTo> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Proceedings+of+the+International+MultiConference+of+Engineers+%26+Computer+Scientists+2013%22">Proceedings of the International MultiConference of Engineers & Computer Scientists 2013</searchLink>. 2013, p1-6. 6p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Rewriting+systems+%28Computer+science%29%22">Rewriting systems (Computer science)</searchLink><br /><searchLink fieldCode="DE" term="%22Machine+theory%22">Machine theory</searchLink><br /><searchLink fieldCode="DE" term="%22Mathematical+logic%22">Mathematical logic</searchLink><br /><searchLink fieldCode="DE" term="%22Control+theory+%28Engineering%29%22">Control theory (Engineering)</searchLink><br /><searchLink fieldCode="DE" term="%22Artificial+intelligence%22">Artificial intelligence</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: OBJ algebraic specification languages support semi-automated verification of algebraic specifications based on equational reasoning by term rewriting systems (TRS). Termination is one of the most important properties of TRSs. Termination guarantees that any execution of the specification terminates in finite times. Another important feature of OBJ languages is a module system with module imports to describe large and complex specifications in a modular way. In this study, we focus on a way to prove termination of OBJ specifications incrementally, based on the notion of modular conditional dependency pairs (MCDP). [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Proceedings of the International MultiConference of Engineers & Computer Scientists 2013 is the property of International Association of Engineers (IAENG) and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=96697248 |
| RecordInfo | BibRecord: BibEntity: Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 6 StartPage: 1 Subjects: – SubjectFull: Rewriting systems (Computer science) Type: general – SubjectFull: Machine theory Type: general – SubjectFull: Mathematical logic Type: general – SubjectFull: Control theory (Engineering) Type: general – SubjectFull: Artificial intelligence Type: general Titles: – TitleFull: Incremental Proofs of Operational Termination with Modular Conditional Dependency Pairs. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Nakamura, Masaki – PersonEntity: Name: NameFull: Ogata, Kazuhiro – PersonEntity: Name: NameFull: Futatsugi, Kokichi IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 03 Text: 2013 Type: published Y: 2013 Titles: – TitleFull: Proceedings of the International MultiConference of Engineers & Computer Scientists 2013 Type: main |
| ResultId | 1 |
