Premium
Reasoning tractably about explicit belief: A model‐theoretic approach
Author(s) -
Sim Kwang Mong
Publication year - 2000
Publication title -
international journal of intelligent systems
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 1.291
H-Index - 87
eISSN - 1098-111X
pISSN - 0884-8173
DOI - 10.1002/1098-111x(200009)15:9<811::aid-int1>3.0.co;2-b
Subject(s) - soundness , decidability , axiom , satisfiability , computer science , completeness (order theory) , class (philosophy) , belief revision , epistemic modal logic , theoretical computer science , model checking , mathematics , artificial intelligence , description logic , multimodal logic , programming language , mathematical analysis , geometry
Abstract Existing epistemic logics such as the logic of implicit and explicit belief and the logic of awareness adopt a deductive‐theoretic approach for characterizing belief. In this approach, an agent represents the state of the world with a conjunction of axioms in its knowledge base (KB) and evaluates queries by trying to prove or disprove that they follow from KB. This paper presents a multivalued epistemic logic (MEL) that allows agents to reason both deductively and model theoretically about implicit and explicit belief. By characterizing an agent's KB with a class of finite models, the set of formulas that an agent believes can be determined by checking their validity in all these models. This rests on the fact that MEL has a complete axiomatization (sentences that are true in all these models will also be provable). In this paper, the soundness, completeness, and decidability of MEL are proven. Furthermore, a polynomial time model‐checking algorithm for determining the satisfiability of a sentence at a particular state in a given model of MEL is also presented. © 2000 John Wiley & Sons, Inc.