Skip to Main content Skip to Navigation
Conference papers

A General Theorem Prover for Quantified Modal Logics

Abstract : The main contribution of this work is twofold. It presents a modular tableau calculus, in the free-variable style, treating the main domain variants of quantified modal logic and dealing with languages where rigid and non-rigid designation can coexist. The calculus uses, to this end, light and simple semantical annotations. Such a general proof-system results from the fusion into a unified framework of two calculi previously defined by the second and third authors. Moreover, the work presents a theorem prover, called GQML-Prover, based on such a calculus. The fair deterministic proof-search strategy used by the prover is described and illustrated via a meaningful example.
Complete list of metadata
Contributor : Virginie Thion Connect in order to contact the contributor
Submitted on : Thursday, January 23, 2014 - 12:06:44 PM
Last modification on : Sunday, June 26, 2022 - 12:00:41 PM
Long-term archiving on: : Thursday, April 24, 2014 - 11:55:30 AM


Files produced by the author(s)




Virginie Thion, Serenella Cerrito, Marta Cialdea. A General Theorem Prover for Quantified Modal Logics. TABLEAUX - Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, 2002, Copenhagen, Denmark. pp.266-280, ⟨10.1007/3-540-45616-3_19⟩. ⟨hal-00935268⟩



Record views


Files downloads