《逻辑、计算和博弈 (4).pdf》由会员分享，可在线阅读，更多相关《逻辑、计算和博弈 (4).pdf（23页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、 LOGIC,COMPUTATION AND GAMES Update with True Information,Picture epistemic model M,s group information state actual world s(seen as such by us as modelers)learning that is true eliminates all -worlds from M s to M|s hard information Update with True Information,Words event!of receiving true new inf
2、ormation is true at actual world,perhaps at others public announcement(or public silence),or just as well public observation(needs no words)update to submodel M|with domain t M|M,t|=simplest case:many other informational events Aside:natural language:“saying that ”,which information?listeners decide
3、 themselves on strength of uptake Three Delicate Dynamic Phenomena not just announcing facts communicating ignorance can be informative:Muddy Children learn facts by learning about their ignorance typical for dynamics:order matters !Kyou p;!p different effect from !p;!Kyou p self-refuting Moore sent
4、ences !(Kp p)may give true information,but you cannot know Kp p Public Announcement Language&Semantics simple pilot system for richer dynamic-epistemic logics PAL language grammar of multi-agent epistemic logic plus !pKp,!(p s)(K1q K2r),!(K1p !qK2r)K3K1s PAL semantics M,s|=!iff if M,s|=,then M|,s|=n
5、ote evaluation in several models at same time PAL Axiom System In technical settings,we often write modal box for K axiom system for PAL 1 all proof principles of multi-agent S5 2 all proof principles of basic modal logic for!plus RE:if|,then|()()3 recursion axioms for postconditions in!:Equivalent
6、Formulation if you do not like the“if is true”conditions use existential dynamic modality :=!recursion axioms once more p (p)()()()K (K()!()(!)Soundness Theorem All provable formulas of PAL are valid.Proof Check what the axioms say Recursion Axiom for New Knowledge M s !M|s M t s (t !Derivations 1 !
7、pKp (p K(p !pp)(p K(p (p p)(p KT)T 2 K(Kp p)KKp Kp Kp Kp T 3 T !T (!T)(T)(T)4 figure this out for yourself&prove Computing Weakest Preconditions there need not be a unique initial model for a given scenario weakest precondition for actions to achieve stated effect Three Cards one possible version “c
8、ards”(R1 W2 B3)!B2!B1K3(K1”cards”K2”cards”K3”cards”)recursion axioms successively compute one epistemic formula as the precondition natural language sometimes says it more economically interplay natural and formal languages huge topic in itself Non-Valid Principles easy to give counterexamples for t
9、he following with concrete formulas and concrete epistemic models !()set =p,=Kp model 1 p-2 p at world 1:!pKp,p,Kp,(p Kp)are true !()set =p,=KBq KBq,=KAq model 1 p,q -A-2 p,q -B-3 p,q At 1:!p!(KBq KBq)KAq false,!(p (KBq KBq)Kaq true also invalid(try yourself)!,!,!Completeness Theorem The provable th
10、eorems of PAL are exactly the valid formulas.Proof Using the recursion axioms each formula can be rewritten step by step to a provably equivalent valid formula in the static epistemic base language.Then use the completeness of the static base logic.Start with innermost occurrences of dynamic modalit
11、ies:iteration recursion axiom not even needed.Decidability and Complexity Theorem PAL is decidable.The completeness argument also gives a decision procedure.However,the reduced static formulas may be exponentially larger than the originals.Theorem The computational complexity of PAL validity and PAL
12、 satisfiability is Pspace-complete.The complexity for the epistemic base logic is Pspace-complete,and also,there is another,polynomial reduction for SAT.Common Knowledge difficulty:!CG has no obvious recursion axiom new notion:conditional common knowledge CG at M,s,this only looks at reachable point
13、s via a path in M that runs entirely along points that satisfy complete axiomatization !CG (CG !)valid,but not enough !CG (CG(!)!)works but we need to extend the axiomatization of static EL+CG Further System Properties schematic validity which principles valid under all substitutions?learning proble
14、m for which formulas is!valid?drop dynamic to static reduction some updates blocked(restricted observation,civilized discourse)in protocol models T not valid,correct law p (T p)reduction to semantic plus procedural information Studying PAL and DEL Sample Open Problem interaction of update and infere
15、nce in PAL !,implies ,but!is usually weaker update e.g.,!does not imply!()gives rise to open problem of Lyndon Theorem for monotonicity inference in PAL.Details explained in Lynd Muddy Children,PAL Programs program structure in communication WHILE you dont know your status!”dont know”;!”I know”;IF T
16、HEN ELSE WHILE DO even|PAL*,Logic of Programmed Conversation add regular program algebra to PAL !;!(composition)!U!(choice)(!)*(iteration)Theorem Validity in PAL*is non-axiomatizable.Proof SAT for PAL*can encode the Recurrent Tiling Problem.Open problem May be wrong modeling,better use the earlier p
17、rotocol models restricting admissible histories of updates:simple decidable logics of conversation analysis/planning?Iterated PAL and Epistemic Temporal Logic Fact PAL(and DEL)translate faithfully into ETL with full future operators,and form simple decidable fragments of these.Also past:!Y with!you
18、learn was true at the previous stage Outlook,Other Updates,Public and Private link cutting Two Envelopes Logic Talk Night Club,you see me open mine email public(cc)and private(bcc)announcement update can now make current model larger:cf.card games trust,lying,cheating Outlook,Updates and Inference r
19、eal agents mix update(observation,communication)and inference 知知 闻 说 亲 knowledge:hearing,proof,experience Moist Logic(+400 BC)You see an object in a dark room and a white object outside the room,someone tells you they have the same color,you infer the object inside is white.Does the PAL proof system describe this real behavior?third person perspective:theory of information flow first person perspective:how agents themselves reason