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
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
https://hal.inria.fr/hal-01244623
Contributor : Stephan Merz <>
Submitted on : Wednesday, December 16, 2015 - 2:20:10 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on: Thursday, March 17, 2016 - 11:20:19 AM

Files

final.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01244623, version 1

Collections

CNRS | INRIA | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Damien Doligez, Jael Kriener, Leslie Lamport, Tomer Libal, Stephan Merz. Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics. Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2014), Aug 2014, Vienna, Austria. pp.1-16. ⟨hal-01244623⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

263

Files downloads

325

 

 

Contact

archive-ouverte@inria.fr