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.
Type de document :
Article dans une revue
Discrete Mathematics and Theoretical Computer Science, DMTCS, 2004, 6 (2), pp.143-162
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00959001
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : jeudi 13 mars 2014 - 17:04:06
Dernière modification le : mercredi 29 novembre 2017 - 10:26:21
Document(s) archivé(s) le : vendredi 13 juin 2014 - 12:10:35

Fichier

dm060201.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

108

Téléchargements de fichiers

361