Skip to Main content Skip to Navigation
Journal articles

Towards automated proofs of observational properties

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, ''\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.
Document type :
Journal articles
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00959001
Contributor : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Submitted on : Thursday, March 13, 2014 - 5:04:06 PM
Last modification on : Wednesday, October 28, 2020 - 2:20:03 PM
Long-term archiving on: : Friday, June 13, 2014 - 12:10:35 PM

File

dm060201.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00959001, version 1

Collections

Citation

Narjes Berregeb, Riadh Robbana, Ashish Tiwari. Towards automated proofs of observational properties. Discrete Mathematics and Theoretical Computer Science, DMTCS, 2004, 6 (2), pp.143-162. ⟨hal-00959001⟩

Share