This paper presents a sound and complete free-variable tableau calculus for constant-domain quantified modal logics, with a propositional analytical basis, i.e. one of the systems K, D, T, K4, S4. The calculus is obtained by addition of the classical free-variable γ-rule and the "liberalized" δ+-rule [14] to a standard set of propositional rules. Thus, the proposed system characterizes proof-theoretically the constant-domain semantics, which cannot be captured by "standard" (non-prefixed, non-annotated) ground tableau calculi. The calculi are extended so as to deal also with non-rigid designation, by means of a simple numerical annotation on functional symbols, conveying some semantical information about the worlds where they are meant to be interpreted. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Cerrito, S., & Mayer, M. C. (2001). Free-variable tableaux for constant-domain quantified modal logics with rigid and non-rigid designation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 137–151). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_11
Mendeley helps you to discover research relevant for your work.