Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics

Damien Doligez 1, 2 Jael Kriener 2 Leslie Lamport 3 Tomer Libal 2 Stephan Merz 2, 4
1 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
2 MSR - INRIA - Microsoft Research - Inria Joint Centre
3 Microsoft Research [Redmond]
4 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : We present a syntactic abstraction method to reason about first-order modal logics by using theorem provers for standard first-order logic and for propositional modal logic.
Type de document :
Communication dans un congrès
Christoph Benzmüller and Jens Otten. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. 33, pp.1-16, 2015
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01244623
Contributeur : Stephan Merz <>
Soumis le : mercredi 16 décembre 2015 - 14:20:10
Dernière modification le : mardi 19 février 2019 - 15:40:03
Document(s) archivé(s) le : jeudi 17 mars 2016 - 11:20:19

Fichiers

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

Identifiants

  • HAL Id : hal-01244623, version 1

Collections

INRIA | UNIV-LORRAINE | LORIA-FM | LORIA | INRIA-ROCQ

Citation

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz. Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. Christoph Benzmüller and Jens Otten. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. 33, pp.1-16, 2015. 〈hal-01244623〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

222

Téléchargements de fichiers

222

Contact


archive-ouverte@inria.fr