A general theorem prover for quantified modal logics. 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, which is accessible in the Internet. The fair deterministic proof-search strategy used by the prover is described and illustrated via a meaningful example.
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Cantone, Domenico; Nicolosi-Asmundo, Marianna: A sound framework for $\delta$-rule variants in free-variable semantic tableaux (2007)
- Thion, V.; Cerrito, S.; Cialdea Mayer, Marta: A general theorem prover for quantified modal logics (2002)