A Set-Theoretic Approach to Automated Deduction in Graded Modal Logics

Abstract

In the paper, we consider the problem of supporting automated reasoning in a large class of knowledge representation formalisms, including terminological and epistemic logics, whose distinctive feature is the ability of representing and reasoning about finite quantities. Each member of this class can be represented using graded modalities, and thus the considered problem can be reduced to the problem of executing graded modal logics. We solve this problem using a set-theoretic approach that first transforms graded modal logics into polymodal logics with infinitely many modalities, and then reduces derivability in such polymodal logics to derivability in a suitable first-order set theory. 1 Introduction The general theme of this paper is the description of a novel approach to the problem of supporting the automation of reasoning in a family of knowledge representation formalisms. Such a family is characterized by the fact that its members need to represent and reason about finite quant...