Automated reasoning with function evaluation for COCOLOG

Suning Wang 1, 2 Peter E. Caines 1, 2
2 MEFISTO
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We introduced a logic for the study of dynamical control systems which we called a Conditional Observer Logic for finite machines (Cocolog). In that paper the properties of consistency and completeness for each first order logical theory in the tree of such theories in a Cocolog were established. The efficacy of automatic theorem proving is a crucial issue in the implementation of Cocolog. In this paper, we present a function evaluation based resolution, called FE-resolution, for Cocolog. The unique model property of Cocolog is first proved via the complete axiomatization property and then the decidability property of any theory in a Cocolog is deduced. Finally, completeness and complexity reduction of FE-resolution is discussed in terms of relative truthfulness and validity.
Type de document :
Rapport
[Research Report] RR-1713, INRIA. 1992
Liste complète des métadonnées

https://hal.inria.fr/inria-00076951
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 11:40:14
Dernière modification le : samedi 27 janvier 2018 - 01:31:33
Document(s) archivé(s) le : vendredi 13 mai 2011 - 22:11:57

Fichiers

Identifiants

  • HAL Id : inria-00076951, version 1

Collections

Citation

Suning Wang, Peter E. Caines. Automated reasoning with function evaluation for COCOLOG. [Research Report] RR-1713, INRIA. 1992. 〈inria-00076951〉

Partager

Métriques

Consultations de la notice

112

Téléchargements de fichiers

70