Narjes Berregeb ; Riadh Robbana ; Ashish Tiwari - Towards automated proofs of observational properties

dmtcs:331 - Discrete Mathematics & Theoretical Computer Science, January 1, 2004, Vol. 6 no. 2 -
Towards automated proofs of observational properties

Authors: Narjes Berregeb 1; Riadh Robbana 1; Ashish Tiwari 2

  • 1 Laboratoire d'Informatique, de Parallélisme et de Productique
  • 2 SRI International [Menlo Park]

Observational theories are a generalization of first-order theories where two objects are observationally equal if they cannot be distinguished by experiments with observable results. Such experiments, called contexts, are usually infinite. Therfore, we consider a special finite set of contexts, called cover-contexts, ''\emphcovering'' all the observable contexts. Then, we show that to prove that two objects are observationally equal, it is sufficient to prove that they are equal (in the classical sense) under these cover-contexts. We give methods based on rewriting techniques, for constructing such cover-contexts for interesting classes of observational specifications.

Volume: Vol. 6 no. 2
Published on: January 1, 2004
Imported on: March 26, 2015
Keywords: observational,contexts,rewriting,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

Linked publications - datasets - softwares

Source : ScholeXplorer IsRelatedTo DOI 10.1007/bf01177550
  • 10.1007/bf01177550
A comparative study

Consultation statistics

This page has been seen 232 times.
This article's PDF has been downloaded 159 times.