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.
Type de document :
Communication dans un congrès
TABLEAUX - Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, 2002, Copenhagen, Denmark. pp.266-280, 2002, 〈10.1007/3-540-45616-3_19〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00935268
Contributeur : Virginie Thion <>
Soumis le : jeudi 23 janvier 2014 - 12:06:44
Dernière modification le : jeudi 11 janvier 2018 - 06:20:11
Document(s) archivé(s) le : jeudi 24 avril 2014 - 11:55:30

Fichier

thio-cial-cerr-Tableaux2002.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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, 2002, 〈10.1007/3-540-45616-3_19〉. 〈hal-00935268〉

Partager

Métriques

Consultations de la notice

250

Téléchargements de fichiers

72