حساب رشته اي و حذف برش براي منطق شهودي شناختي ديناميك

چكيده انگليسي :

Sequent calculus and cut elimination for Intuitionistic Dynamic Epistemic Logic MINA MORADI RIZI mina moradi@math iut ac ir September 18 2013 Master of Science Thesis in Farsi Departement of Mathematical Sciences Isfahan University of Technology Isfahan 84156 83111 IranSupervisor Dr Mojtaba Aghaei aghaei@cc iut ac ir2010 MSC 05C15 53C42Keywords Dynamic epistemic logic Adjoint modalities Cut elimination Nested Admissibility of cut Abstract This M Sc thesis is based on the following paper Roy Dyckhoff Mehrnoosh Sadrzadeh Julien Truffaut Algebra Proof Theory and Applications for an Intu itionistic Logic of Propositions Actions and Adjoint Modal Operators ACM Trans Comput Logic 666 0 2013 38 pages Epistemic logics can express properties of programs and distributed system protocols The modalities of epistemiclogics encode attitudes such as knowledge and belief but dynamic changes to these attitudes after actions such asannouncements have traditionally been formalised only in a semantic fashion Adding epistemic modalities to dy namic logics led to logics allowing reasoning about belief updates both syntactically and semantically But lackingcut admissibility the calculus proposed in 4 is not a basis for automatic proof search As always the presence ofa cut rule would ensure infinite non determinism in proof search so we have to avoid it its admissibility is how ever important for completeness Likewise we incorporate weakening and contraction into our logical rules whileensuring for completeness sake that they are admissible rather than having them as primitive thus reducing thenon determinism even further Here we develop a cut free sequent calculus as basis for a proof search procedure forone such logic The logic comprises a linear logic Q of actions and a logic M of propositions The modalities of the logic include thedynamic modality known as the weakest precondition and its right adjoint the strongest postcondition We presentan algebraic semantics for these logics in terms of a pair of a residuated lattice monoid of actions and its lattice ofpropositions We endow both Q and M with families of epistemic adjoint operators satisfying distributivity propertiesover the operations of the action logic propositional logic and their dynamic modalities We present appropriatesequent calculus rules for these modalities First a logic for actions is presented whose language contains connectives for combining actions and two adjointmodalities A and A We read A q as the appearance to agent A of action q and A q as A s belief that ithappens The algebraic semantic of this logic in 1 is given by a lattice monoid with adjoint modalities LMAM Moreover a nested sequent calculus for this logic is provided and then we establish the admissibility of the cut rule Inaddition a logic for propositions is developed whose language similar to the previous logic consists of connectivesfor combining propositions two adjoint modalities A and A and two modal dynamic operators q and q The semantics of this logic in 1 is given by Heyting algebra with adjoint modalities HAAM Finally a cut freenested sequent calculus by adding some rules corresponding to the connectives adjoint modal operators and modaldynamic operators to the sequent calculus for actions logic is presented The operator q is the dynamic modalityoperator and q m is read as after action q proposition m holds q is its left adjoint called update A is theleft adjoint of A The former is the uncertainty of an agent about a proposition the latter is his belief A m is readas A believes that m

مرادي ريزي،م مينا

حساب رشته اي و حذف برش براي منطق شهودي شناختي ديناميك

منطق شناختي ديناميك , موجهات الحاقي , حذف قاعده ي برش , تودرتو , پذيرفتني بودن قاعده ي برش