In this paper we describe an algorithmic framework for a multi-modal logic arising from the combination of the system of modal (epistemic) logic devised by Meyer and van der Hoek for dealing with nonmonotonic reasoning with a deontic logic of the Jones and Porn-type. The idea behind this (somewhat eclectic) formal set-up is to have a modal framework expressive enough to model certain kinds of deontic defeasibility, in particular by taking into account preferences on norms. The appropriate inference mechanism is provided by a tableau-like modal theorem proving system which supports a proof method closely related to the semantics of modal operators. We argue that this system is particularly well-suited for mechanizing nonmonotonic forms of inference in a monotonic multi-modal setting.
展开▼
机译：在本文中，我们描述了一种多模态逻辑的算法框架，该算法框架是由梅耶（Meyer）和范德霍克（van der Hoek）设计的模态（流行病）逻辑系统的组合产生的，该系统用于处理非单调推理以及琼斯和色情类型的道义逻辑。 。这种（有些折衷的）正式设置背后的想法是要有一个足够表达的模态框架，以对某些类型的宗法可废性进行建模，特别是要考虑对规范的偏好。类似于表格的模态定理证明系统提供了适当的推理机制，该系统支持与模态算子的语义紧密相关的证明方法。我们认为该系统特别适合在单调多模态环境中机械化非单调形式的推理。
展开▼
