Theory matrices (for modal logics) using alphabetical monotonicity |
| |
Authors: | Ian P. Gent |
| |
Affiliation: | (1) Department of Artificial Intelligence, University of Edinburgh, EH1 1HN Edinburgh, Scotland |
| |
Abstract: | In this paper I give conditions under which a matrix characterisation of validity is correct for first order logics where quantifications are restricted by statements from a theory. Unfortunately the usual definition of path closure in a matrix is unsuitable and a less pleasant definition must be used. I derive the matrix theorem from syntactic analysis of a suitable tableau system, but by choosing a tableau system for restricted quantification I generalise Wallen's earlier work on modal logics. The tableau system is only correct if a new condition I call alphabetical monotonicity holds. I sketch how the result can be applied to a wide range of logics such as first order variants of many standard modal logics, including non-serial modal logics. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|