Discrete Mathematics & Theoretical Computer Science
Volume 6 n° 1 (2004), pp. 143-162
| author: | Narjes Berregeb and Riadh Robbana and Ashish Tiwari |
|---|---|
| title: | Towards automated proofs of observational properties |
| keywords: | observational, contexts, rewriting |
| abstract: | 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, ``covering'' 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. If your browser does not display the abstract correctly (because of the different mathematical symbols) you can look it up in the PostScript or PDF files. |
| reference: | Narjes Berregeb and Riadh Robbana and Ashish Tiwari (2004), Towards automated proofs of observational properties, Discrete Mathematics and Theoretical Computer Science 6, pp. 143-162 |
| bibtex: | For a corresponding BibTeX entry, please consider our BibTeX-file. |
| ps.gz-source: | dm060201.ps.gz (66 K) |
| ps-source: | dm060201.ps (191 K) |
| pdf-source: | dm060201.pdf (119 K) |
The first source gives you the `gzipped' PostScript, the second the plain PostScript and the third the format for the Adobe accrobat reader. Depending on the installation of your web browser, at least one of these should (after some amount of time) pop up a window for you that shows the full article. If this is not the case, you should contact your system administrator to install your browser correctly.
Due to limitations of your local software, the two formats may show up differently on your screen. If eg you use xpdf to visualize pdf, some of the graphics in the file may not come across. On the other hand, pdf has a capacity of giving links to sections, bibliography and external references that will not appear with PostScript.
Automatically produced on Sun Jan 18 16:32:20 CET 2004 by falk