WWW.DISSERTATION.XLIBX.INFO FREE ELECTRONIC LIBRARY - Dissertations, online materials

<< HOME
CONTACTS

Pages:   || 2 | 3 | 4 |

# «Abstract. We develop clausal tableau calculi for seven multimodal logics variously designed for reasoning about multi-degree belief, reasoning about ...»

-- [ Page 1 ] --

Clausal Tableaux for Multimodal Logics of Belief

Rajeev Gor´1 and Linh Anh Nguyen2

e

1

The Australian National University and NICTA

Canberra ACT 0200, Australia

Rajeev.Gore@anu.edu.au

2

Institute of Informatics, University of Warsaw

ul. Banacha 2, 02-097 Warsaw, Poland

nguyen@mimuw.edu.pl

Abstract. We develop clausal tableau calculi for seven multimodal logics variously

of belief and for reasoning about epistemic states of agents in multi-agent systems.

Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, thereby giving decision procedures for all of these logics. We also use our calculi to obtain complexity results for ﬁve of these logics. The complexity of one was known and that of the seventh remains open.

Keywords: modal logics for agent-based systems, theorem proving for modal logics, complexity and decidability of modal and temporal logics.

1 Introduction Modal logics have been widely studied for reasoning about knowledge and belief, usually based on the monomodal logics S 5 and KD45 for reasoning about knowledge and belief respectively. Both logics have the axioms 4 : 2ϕ → 22ϕ and 5 : ¬2ϕ → 2¬2ϕ, which mean that knowledge and belief both satisfy positive and negative introspection. The logic S 5 also has the axiom T : 2ϕ → ϕ, which means that knowledge is veridical, while KD45 also has the axiom D : 2ϕ → ¬2¬ϕ, which means that belief is consistent.

For multiple agents, the usual solution is to use a multimodal logic which has m pairs of modal operators 2i and 3i, for some ﬁxed number m. The base multimodal logics for reasoning about knowledge and belief are typically S5(m) and KD45(m), respectively, where each pair 2i and 3i is of type S5 and KD45, usually with no interactions between modal operators of diﬀerent indices (see, e.g., [14, 8, 22, 35]). An alternative is to use S 5 and KD45 type modalities labelled with agent terms [10], again without interaction axioms.

When the knowledge and beliefs of multiple agents interact then interactions between the modalities are used. One approach is to use bi-modal logics with inter- actions [33, 27]. Another is to extend the multimodal grammar logics of Fari˜as del n Cerro and Penttonent [5] with (seriality) axioms D for reasoning about knowledge and belief. Recall that a grammar logic is a multimodal logic with axioms of the form [s1 ]... [sn ]ϕ → [t1 ]... [tm ]ϕ, where [si ] and [tj ] are universal (box-like) modal operators labelled by constants si and tj, respectively (see [2, 3, 6, 34, 16, 7, 12]).

National ICT Australia (NICTA) is funded through the Australian Government’s Backing Australia’s Ability initiative, in part through the Australian Research Council.

For knowledge distributed over groups of agents there is the well-known multimodal logic of common knowledge and distributed knowledge among a group of agents (see [14, 8, 22]) as well as a similar logic for reasoning about mutual beliefs of agents [1]. There are also multi-modal logics of dynamic belief and knowledge for use in multi-agent systems [20, 32].

We concentrate on seven speciﬁc multimodal logics of belief, studied by Nguyen in the context of modal logic programming and modal deductive databases [28, 30].

They are introduced in Section 2.2 as:

KDI4, KDI4s, KDI4s 5, KDI45 for reasoning about multi-degree belief;

KD4s 5s for reasoning about distributed systems of belief; and KD45(m), KD4Ig 5a for reasoning about epistemic states of agents in multi-agent systems.

All except KD45(m) contain interaction axioms. Both KDI4 and KDI4s are grammar logics extended with axiom D.

Tableau methods have been successively applied to modal logics to give decision procedures (see, e.g., [9, 13, 3, 35, 11, 19, 18]). There are also tableau calculi for a number of multimodal logics of knowledge and/or belief, e.g., [3, 35, 10]. But [3] concerns only grammar logics, while [35, 10] lack interaction axioms between modal operators of diﬀerent indices. As far as we know, only KDI4 and KD45(m) from the seven multimodal logics (listed above) have labelled tableau calculi [3, 35]. We know of no non-labelled tableau calculi for any of these logics although Shvarts’ calculus for KD45 from [11] can be extended trivially to KD45(m). Nor do we know of any tableau calculus for the multimodal logic of mutual belief introduced by Aldewereld et al. [1], which is similar to our KD4s 5s.

Here, we develop (non-labelled) tableau calculi for all seven of the above multimodal logics of belief. Our tableau calculi are sound, complete, cut-free and have the analytic superformula property, so they are decision procedures.

Our tableau calculi require clausal form and are called clausal tableau calculi.

Transformation to clauses was ﬁrst used for sequent calculi by Mints [23] and Hudelmaier [17] and then applied to tableau calculi by Nguyen [24]. Hudelmaier and Nguyen showed that clausal form can give better space bounds and improved decision procedures for some modal logics [17, 24]. We show that clauses can also simplify the task of developing tableau calculi for certain modal logics by giving clausal tableau calculi for the complicated logics KDI45 and KD4Ig 5a. Finally, we show that our tableaux can be used to estimate the complexity of the satisﬁability problem in ﬁve of the multimodal logics we consider: NP-complete for KDI4s 5, KD4s 5s, KDI45, and PSPACE-complete for KDI4 and KDI4s. The complexity for KD45(m) is known to be PSPACE-complete [14]. We do not have an exact complexity result for KD4Ig 5a.

The rest of this paper is organized as follows. In Section 2, we specify the seven multimodal logics of belief and give deﬁnitions for tableau calculi. In Section 3, we deﬁne modal clauses and consider transformation to clauses. In Section 4, we present our tableau calculi and prove their soundness. In Section 5, we prove completeness of the calculi. Section 6 deals with the complexity of the logics. Section 7 contains concluding remarks.

–  –  –

2.1 Deﬁnitions for Multimodal Logics We consider multimodal logics with m pairs of modal operators 2i and 3i, where 1 ≤ i ≤ m. We use p and q to denote primitive propositions. Formulae of our language

are recursively deﬁned using the BNF grammar below:

–  –  –

We say that ϕ is satisﬁed at w in M if M, w ϕ. We say that ϕ is satisﬁed in M, and write M ϕ, and call M a model of ϕ, if M, τ ϕ.

If we allow all Kripke models (with no restrictions on the accessibility relations) then we obtain a multimodal logic which has a standard Hilbert-style axiomatisation denoted by K(m). Other normal multimodal logics are obtained by adding certain axioms to K(m).

Suppose a normal ﬁrst-order deﬁnable modal logic L is characterised by a class C of Kripke frames. The ﬁrst order formulae describing C are L-frame restrictions, and any frame in C is an L-frame. A model M is an L-model if its underlying frame is an L-frame. We say that ϕ is L-satisﬁable if there exists an L-model of ϕ, i.e. an L-model satisfying ϕ. A formula ϕ is said to be L-valid and called an L-tautology if ϕ is true in every L-model.

–  –  –

In the above systems, the axiom (I) gives 2i ϕ the meaning “ϕ is believed up to degree i”, and 3i ϕ can be read as “it is possible weakly at degree i that ϕ”. The axioms (5) are controversial as they are quite strong. For this reason, we consider also KDI4 and KDI4s. Note that the axiom (5s ) is derivable in KDI4s 5.

Although the logic KDI4 belongs to the class of logics considered by Debart et al. [4] (for multimodal logic programming) and the axioms I and 4s are possible axioms for grammar logics, the reading of modal indices as degrees of belief has not been considered by other authors. Our logics of multi-degree belief are similar to graded modal logics [22], where grades constrain the number of worlds accessible from the current world, but our degrees of belief are symbolic rather than numeric.

For multi-agent systems, we use subscripts on 2 and 3 to denote agents and assume that 2i ϕ stands for “agent i believes that ϕ is true” and 3i ϕ stands for “ϕ is considered possible by agent i”. For distributed systems of belief we can use the logic system KD4s 5s = K(m) + (D) + (4s ) + (5s ) In this system, all agents have full access to the belief bases of other agents: they are united as “friends”. Our logic KD4s 5s has features similar to the logic S5P(m) introduced by Meyer and van der Hoek [21], but S5P(m) is intended for formalising preference and the operators Pi of [21] need not be serial.

In another kind of multi-agent system, agents are “opponents” who play against each other, and each agent may want to simulate the epistemic states of the others.

To write a program for one agent, we may need to use modal operators of the other

agents. A suitable logic for this problem is:

KD45(m) = K(m) + (D) + (4) + (5)

As mentioned earlier, the logic KD45(m) has been intensively studied. We use a subscript in KD45(m) to distinguish the logic from the monomodal logic KD45, while there is not such a need for the other considered multimodal logics.

To capture common belief of a group of agents, one can extend the logic KD45(m) with modal operators for groups of agents and some additional axioms. Suppose that there are n agents and m = 2n − 1. Let g be an one-to-one function that maps every natural number less than or equal to m to a non-empty subset of {1,..., n}.

Suppose that an index 1 ≤ i ≤ m stands for the group of agents whose indices form the set g(i). We can adopt the axioms (D), (4), and additionally (Ig ) : 2i ϕ → 2j ϕ if g(i) ⊃ g(j), so i indicates a group that contains the group identiﬁed by j, and (5a ) : ¬2i ϕ → 2i ¬2i ϕ if g(i) is a singleton, so that i stands for an agent. Thus, for

reasoning about belief and common belief, we can use:

KD4Ig 5a = K(m) + (D) + (4) + (Ig ) + (5a )

4 Here we want to catch the most important properties of belief and common belief, and the aim is not to give an exact formulation of belief or common belief. This logic is therefore diﬀerent in nature from the well-known multimodal logics of common knowledge with ﬁxed-points. It also diﬀers from the multimodal logic of mutual belief introduced by Aldewereld et al. [1]. Our modal operator of common belief satisﬁes positive introspection, while the operator of mutual belief introduced in [1] lacks this property. On the other hand, the latter operator has some properties that the former does not have.

The given axioms correspond to the following frame restrictions:

–  –  –

2.3 Deﬁnitions for Tableau Calculi As in our previous works on tableau calculi [11, 27, 12], our tableau formulation traces their roots to Hintikka via [31]. A tableau rule σ consists of a numerator N above the line and a (ﬁnite) list of denominators D1, D2,..., Dk (below the line) separated by vertical bars. The numerator is a ﬁnite formula set, and so is each denominator. As we shall see later, each rule is read downwards as “if the numerator is L-satisﬁable, then so is one of the denominators”. The numerator of each tableau rule contains one or more distinguished formulae called the principal formulae. A tableau calculus CL for a logic L is a ﬁnite set of tableau rules.

A CL-tableau for X is a tree with root X whose nodes carry ﬁnite formula sets obtained from their parent nodes by instantiating a tableau rule with the proviso that if a child s carries a set Z and Z has already appeared on the branch from the root to s then s is an end node.

Let ∆ be a set of tableau rules. We say that Y is obtainable from X by applications of rules from ∆ if there exists a tableau for X which uses only rules from ∆ and has a node that carries Y. A branch in a tableau is closed if its end node carries only ⊥.

A tableau is closed if every one of its branches is closed. A tableau is open if it is not closed. A ﬁnite formula set X is CL-consistent if every CL-tableau for X is open. If there is a closed CL-tableau for X then X is CL-inconsistent.

A tableau calculus CL is sound if for all ﬁnite formula sets X, if X is L-satisﬁable then X is CL-consistent. It is complete if for all ﬁnite formula sets X, if X is CLconsistent then X is L-satisﬁable. Let σ be a rule of CL. We say that σ is sound w.r.t. L if for every instance σ of σ, if the numerator of σ is L-satisﬁable then so is one of the denominators of σ. Any CL containing only rules sound w.r.t. L is sound.

53 Modal Clauses

A classical literal is a formula of the form p or ¬p, where p is a primitive proposition.

We use a, b, c to denote classical literals, and to denote a possibly empty sequence of universal (box-like) modal operators, which is also called a universal modality. We write [ϕ1,..., ϕk ] to denote (ϕ1 ∨... ∨ ϕk ) with the emphasis that the order of disjuncts is not important.

A (modal) clause is a formula of the form [a1,..., ak ], [a, 2i b], [a, 3i b], or 3i b, where is called the modal context.

Proposition 1. Every formula set can be transformed in quadratic time to a set of clauses which is equisatisﬁable in any normal modal logic to the ﬁrst set.

Proof. Repeatedly replace a complex formula by a new primitive proposition which is “deﬁned” by that formula (see, e.g., [23, 17, 24]). For example, (ϕ ∨ 3i ψ), where ψ is not a primitive proposition, is replaced by (ϕ ∨ 3i p) and 2i (¬p ∨ ψ), where p is a fresh primitive proposition (deﬁning ψ via the second added clause). We need to do at most n such replacements, where n is the sum of the lengths of formulae belonging to the input set. Hence the transformation can be done in quadratic time.

We now deﬁne L-clauses using a case-distinction on L as:

For L ∈ {KDI4, KDI4s, KD4Ig 5a }: every clause is an L-clause;

For L ∈ {KD4s 5s, KDI4s 5}: an L-clause is a clause with modal depth 1 or 0;

Pages:   || 2 | 3 | 4 |

Similar works:

«Climate-KIC: CAPplan Reporting GA2012 (Version 0.6) CAPplan Guidance Notes Cost reporting GA2012 Performance reporting GA2012 1/50 Climate-KIC: CAPplan Reporting GA2012 (Version 0.6) Table of Contents 1. Introduction 1.1 General 1.2 Leadership & role of the CLC directors and contacts 1.3 Timeline and deadlines for submission 1.4 Formats for submission: electronic and signed hardcopy 1.5 CFS: Audit certification & sampling by EIT 1.6 Period Covered and relevant Business Plan 1.7 Link to...»

«Children’s Hospital of Michigan Family Information Guide Table of Contents About Us We believe in family-centered care More About Us We’re a teaching and research hospital While You’re Here Tips for a better hospital stay Children’s Feelings The emotional side of being in the hospital TV and Movies Where to find kid-friendly shows Pain How much is too much? Who’s Who? Doctors, nurses and other people you’ll meet While You’re Here Things you’ll need to bring and know The Library...»

«St Mary’s University, Twickenham Board of Governors Minutes of a meeting of the Board of Governors held on Thursday 26th November 2015 in the Shannon suite, St Mary’s University, Twickenham.Present: Rt Rev Richard Moth (Chair) Sir Anthony Bailey Mr Francis Campbell (Vice-Chancellor) Mr John Dixon Fr Richard Finn Mr Mike Foster (to M10 only) Dr Maureen Glackin Mrs Sue Handley-Jones Mr David Hartnett Mrs Maureen John Mr Stuart Kemp Mr Zander Lavall (President of SMSU) Dr David Livesey Mr...»

«10.2.1 CHAPTER 10.2 Parasitic infections of the skin John M. Goldsmid and Wayne Melrose 10.2.1 INTRODUCTION A wide range of parasitic infections can involve the skin and subcutaneous tissues. Depending on the species of parasite, this involvement may be transient, the parasite passing through the skin on its migration to the blood stream and so to a specific target organ, or the infection may be localised to the skin. In the latter infections, the skin may be the primary site of infection or...»

«THE OTHER DAUGHTER CHAPTER ONE Twenty years later She was late, she was late, oh, God, she was so late! Melanie Stokes came bounding up the stairs, then made the hard left turn down the hall, her long blond hair whipping around her face. Twenty minutes and counting. She hadn't even thought about what she was going to wear. Damn. She tore into her room with her sweatshirt half pulled over her head. A strategic kick sent the heavy mahogany door slamming shut behind her as she shed the first layer...»

«Museivännen Medlemsblad för museets vänner, Ljusdalsbygdens museum Nr 2 2010 Lösnummerpris 10 kr 1 Föreningen Museets vänner Museets vänners styrelse Ledamöter Karin Esbjörnsson, ordf Elisabeth Fransson, v ordf Siv Kram, kassör sekr, vakant Margareta Ivarsson Owe Norberg, museichefen är självskriven ledamot Ersättare Birgitta Anvret Elli Genberg Sigyn Söderström Adjungerade ledamöter Gunn Lannås Elsa Sunnefeldt Adress: Ljusdalsbygdens museum Museivägen 5 827 30 Ljusdal Tel:...»

«Performance improvement of headworks: a case of Kalignadaki A Hydropweor Project through physical hydraulic modelling Dr. Ing. Meg B. Bishwakarma General Manager, Hydro Lab Pvt. Ltd., Nepal ABSTRACT: The Kali Gandaki A Hydropower Plant (KGA) is a peaking run-of-river type of project with installed capacity of 144 MW. This is owned and being operated by Nepal Electricity Authority (NEA). Since its operation started in 2002, the headworks of this plant has been experiencing unfavourable...»

«Read e-Book Aeneas World Mythology at Online Library. Get file Aeneas World Mythology PDF to free download AENEAS WORLD MYTHOLOGY PDF Update method of help documentation is really a hard copy manual that's printed, nicely bound, and functional. Itoperates as a reference manual skim the TOC or index, get the page, and stick to the directions detail by detail. The challenge using these sorts of documents is the fact that user manuals can often become jumbled and hard tounderstand. And in order to...»

«UB EPORTFOLIO STARTUP GUIDE ePortfolio GENERAL USER Startup Guide [2016-17] Table of Contents Page 2: Introduction Logging in to your Digication account Page 3: Steps to create an ePortfolio from course template Page 4: Steps to Create from Scratch Steps to Select your Settings Page 8: Steps to Customize your Theme or Change Settings Page 10: Steps to Customize your Directory Icon Adding Content Page 11: Add/Edit tabs Page 13: Adding Modules Page 15: How to work with LARGE MEDIA FILES Page 16:...»

«In Proceedings of the Second International Symposium on End User Development, March 2-4, 2009, Siegen, Germany (to appear). Males’ and Females’ Script Debugging Strategies Valentina Grigoreanu1,2, James Brundage2, Eric Bahna2, Margaret Burnett1, Paul ElRif2, Jeffrey Snover2 1 Oregon State University, School of Electrical Engineering and Computer Science, Corvallis, Oregon, USA 97331 {grigorev, burnett}@eecs.oregonstate.edu 2 Microsoft, One Microsoft Way, Redmond, Washington, USA {t-valeng,...»

«UNIONE ACCADEMICA NAZIONALE Corpus dei Manoscritti Copti Letterari LETTERATURA COPTA Serie Studi TITO ORLANDI COPTIC TEXTS RELATING TO THE VIRGIN MARY An Overview Roma CIM 2008 The layout has been prepared by the author, using troff/groff for layout and postscript fonts. God bless Unix/Linux and Gnu. © CIM Roma ISBN 88-85354-08-4 CONTENTS I. Generalia 5 a) Introduction, 5 — b) Terminology, 7 — c) Classiﬁcation of works and fragments, 12 II. Bibliological and Codicological Units 13 1. The...»

«Hibiscus International The Official Publication of the International Hibiscus Society www.internationalhibiscussociety.org Volume 8, Number 3, Issue No.36 July, August & September 2008 EDITOR: Richard Johnson, Tahiti, French Polynesia diveta@mail.pf INDEX From The Presidents by Richard Johnson.. 2 From The Editor: Richard Johnson.. 2 Secretary/Treasurers Report: Wayne Hall.. 3 Board Of Directors.. 3 Treasury.. 4 Committee Reports EIHF: Executive International Hibiscus Forum. 5 IHS...»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.