Clausal resolution for normal modal logics |
| |
Authors: | Cludia Nalon Clare Dixon |
| |
Institution: | aDepartamento de Ciência da Computação, Universidade de Brasília, Caixa Postal 4466, CEP:70.910-090, Brasília, DF, Brazil;bDepartment of Computer Science, University of Liverpool, Liverpool, L69 3BX, United Kingdom |
| |
Abstract: | We present a clausal resolution-based method for normal modal logics. Differently from other approaches, where inference rules are based on the syntax of a particular set of axioms, we focus on the restrictions imposed on the binary accessibility relation for each particular normal logic. We provide soundness and completeness results for all fifteen families of multi-modal normal logics whose accessibility relations have the property of being non-restricted, reflexive, serial, transitive, Euclidean, or symmetric. |
| |
Keywords: | Normal modal logics Automated deduction Resolution |
本文献已被 ScienceDirect 等数据库收录! |
|