Berregeb, Narjes; Robbana, Riadh; Tiwari, Ashish Towards automated proofs of observational properties. (English) Zbl 1036.68062 Discrete Math. Theor. Comput. Sci. 6, No. 1, 143-162 (2003). Summary: 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. MSC: 68Q42 Grammars and rewriting systems 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:observational; contexts; rewriting PDF BibTeX XML Cite \textit{N. Berregeb} et al., Discrete Math. Theor. Comput. Sci. 6, No. 1, 143--162 (2003; Zbl 1036.68062) Full Text: EuDML EMIS OpenURL