TY - GEN
T1 - OBSERVANT: an Annotated Term Rewriting System for Deciding Observation
AU - Monroy,R.
AU - Bundy,Alan
AU - Green,I.
PY - 1998
Y1 - 1998
N2 - 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.
AB - 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.
M3 - Conference contribution
SP - 393
EP - 397
BT - Proceedings of the 13th European Conference on Artificial Intelligence (ECAI-98)
ER -