Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment

DOI10.1007/978-3-319-73579-5_9zbMath1503.68180OpenAlexW2782410730MaRDI QIDQ1742627

Sophie Pinchinat, Tristan Charrier, François Schwarzentruber

Publication date: 12 April 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-73579-5_9

Mathematics Subject Classification ID

Logics of knowledge and belief (including belief change) (03B42) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• TPTP
• z3
• CVC4
• iProver

This page was built for publication: Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment