Interactive Theorem Proving with Temporal Logic

Amy Felty 1 Laurent Théry
1 CROAP - Design and Implementation of Programming Tools
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : In this paper, we present a theorem prover for linear temporal logic. Our goal is to extend the capabilities of existing interactive and automatic systems for verifying temporal properties of software and hardware systems. We focus on increasing the effectiveness of user interaction in such systems. In particular, we extend the techniques of {\em proof by pointing} and {\em point and shoot} for mouse-driven proof construction in first-order logic to temporal logic. In addition, we show how to generate text from proofs by extending a previously given translation for first-order logic to the temporal operators. Our theorem prover implements an inference system for temporal logic that we have defined. The inference rules of this system are more intuitive than the rules commonly given for temporal logics and thus they are better suited to our goals. We present this inference system and prove that it is sound and complete with respect to a known system.
Type de document :
RR-2804, INRIA. 1996
Liste complète des métadonnées

Littérature citée [2 références]  Voir  Masquer  Télécharger
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:59:41
Dernière modification le : samedi 27 janvier 2018 - 01:31:30
Document(s) archivé(s) le : jeudi 24 mars 2011 - 13:12:22



  • HAL Id : inria-00073886, version 1



Amy Felty, Laurent Théry. Interactive Theorem Proving with Temporal Logic. RR-2804, INRIA. 1996. 〈inria-00073886〉



Consultations de la notice


Téléchargements de fichiers