Edinburgh Research Explorer

OBSERVANT: an Annotated Term Rewriting System for Deciding Observation

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

Original languageEnglish
Title of host publicationProceedings of the 13th European Conference on Artificial Intelligence (ECAI-98)
Pages393-397
StatePublished - 1998
Event13th European Conference on Artificial Intelligence, Brighton, UK, August 23-28 1998, Proceedings - Brighton, United Kingdom
Duration: 23 Aug 199828 Aug 1998

Conference

Conference13th European Conference on Artificial Intelligence, Brighton, UK, August 23-28 1998, Proceedings
CountryUnited Kingdom
CityBrighton
Period23/08/9828/08/98

Abstract

The use of term-rewriting systems (TRSs) is at the core of automated theorem proving (ATP). There are a number of methods whereby we can build terminating TRSs with full deduction power, with respect to some theory. Yet, there exist theories these techniques cannot handle, giving rise to a trade-off between deduction power and termination. One such theory is the theory of observation congruence [Milner, 1989b] in CCS [Milner, 1989a]. The standard approach to overcome this situation is to use meta-level information; it, however, introduces the problem of finding and capturing such meta-level control. This paper advocates the use of annotated TRSs (ATRSs) for approaching these problems; the annotation are used to capture meta-level information that helps direct proof search, while giving an intuitive account about why and how rewriting is expected to work. We introduce an ATRS, called Observant. Observant is goal-oriented, and, hence domain-specific: it can be used to build a decision procedure for observation congruence in CCS [Milner, 1989a]; furthermore, it can be used to attempt to solve or prove CCS equations, involving either finite-state systems, or infinite-state systems. We prove Observant terminating, sound, and complete - over the normalisation of finite processes. We argue that Observant surpasses rival term-rewriting strategies.

Event

Download statistics

No data available

ID: 25317042