2006 | OriginalPaper | Buchkapitel
Decision Procedure for a Fragment of Mutual Belief Logic with Quantified Agent Variables
verfasst von : Regimantas Pliuškevičius, Aida Pliuškevičienė
Erschienen in: Computational Logic in Multi-Agent Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
A deduction-based decision procedure is presented for a fragment of mutual belief logic with quantified agent variables (
MBQL
). The language of
MBQL
contains belief, everybody believes and mutual belief modalities, variables and constants for agents. The language of
MBQL
is convenient to describe the properties of rational agents when the number of agents is not known in advance. On the other hand, even if the exact number of agents is known, a language with quantified agent variables allows us to use more compact expressions. For the
MBQL
a sequent calculus
MBQ
*
with invertible (in some sense) rules is proposed. The presented decision procedure is realized by means of the calculus
MBQ
*
that allows us to simplify a procedure of loop-check sharply. For a fragment of
MBQL
(without positive occurrences of mutual belief modality), the loop-check-free sequent calculus is proposed. To this end, special rules for belief and everybody believes modalities (introducing marked modalities and indices) and special sequents serving as a termination criterion for non-derivability are introduced. For sequents containing positive occurrences of mutual belief modality sequents of special shape are used to specialize a loop-check and to find non-logical (loop-type) axioms.