BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//SECURITY & APPLIED LOGIC - ECPv6.15.20//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-ORIGINAL-URL:https://sal.cs.unibuc.ro
X-WR-CALDESC:Events for SECURITY & APPLIED LOGIC
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:UTC
BEGIN:STANDARD
TZOFFSETFROM:+0000
TZOFFSETTO:+0000
TZNAME:UTC
DTSTART:20180101T000000
END:STANDARD
END:VTIMEZONE
BEGIN:VTIMEZONE
TZID:Europe/Bucharest
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20170326T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20171029T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20180325T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20181028T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0200
TZOFFSETTO:+0300
TZNAME:EEST
DTSTART:20190331T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0300
TZOFFSETTO:+0200
TZNAME:EET
DTSTART:20191027T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=UTC:20190228T100000
DTEND;TZID=UTC:20190228T120000
DTSTAMP:20260620T150000
CREATED:20190225T044031Z
LAST-MODIFIED:20190225T170129Z
UID:363-1551348000-1551355200@sal.cs.unibuc.ro
SUMMARY:An introduction to BAN logic (a logic of authentication)
DESCRIPTION:Speaker: Alexandru Dragomir (University of Bucharest) \n\nAbstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows\, Abadi & Needham 1989)\, a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs\, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic\, (2) following the original paper’s analysis of the Otway-Rees protocol\, (3) presenting some objections to using BAN\, and (4) discussing the problem of offering a semantics of BAN logic.
URL:https://sal.cs.unibuc.ro/event/an-introduction-to-ban-logic-a-logic-of-authentication/
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=UTC:20190228T100000
DTEND;TZID=UTC:20190228T120000
DTSTAMP:20260620T150000
CREATED:20190225T043808Z
LAST-MODIFIED:20190225T043808Z
UID:361-1551348000-1551355200@sal.cs.unibuc.ro
SUMMARY:The hybridization of many-sorted polyadic modal logic
DESCRIPTION:Speaker: Natalia Moangă (University of Bucharest). \nAbstract: Hybrid logics are obtained by enriching modal logics with nominals and state variables\, that directly refer the individual points in a Kripke model. In the present work we develop a hybrid version on top of our many-sorted polyadic logic\, previously defined. Our system has nominals and state variables on each sort\, as well as binders that act like the universal and the existential quantfiers on state variables. In doing this\, we follow various approaches for hybrid modal logic\, especially the work of Blackburn and Tsakova.
URL:https://sal.cs.unibuc.ro/event/the-hybridization-of-many-sorted-polyadic-modal-logic/
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=UTC:20190131T100000
DTEND;TZID=UTC:20190131T120000
DTSTAMP:20260620T150000
CREATED:20190127T174249Z
LAST-MODIFIED:20190127T174249Z
UID:284-1548928800-1548936000@sal.cs.unibuc.ro
SUMMARY:The frontier between decidability and undecidability for logics for strategic reasoning in the presence of imperfect information
DESCRIPTION:Speaker:   Catalin Dima (Université Paris-Est Créteil.) \n\nAbstract: \nThe last 15-20 years have seen a number of logical formalisms that focus on strategic reasoning. These logics aim at giving specification languages for various multi-agent game structures\, in which agents have adversarial or cooperative objectives which may be qualitative or quantitative and may have various types of imperfect information. The presence of imperfect information raises a particular difficulty in that many games cannot be solved algorithmically\, as well as their corresponding logical formalisms. In this tutorial I will review some techniques for proving that the Alternating-time Temporal Logic has an undecidable model-checking problem\, but this problem becomes decidable when considering memoryless strategies\, coalitions with distributed knowledge\, hierarchical knowledge and public or coalition-public announcements. I will also give a short introduction to the model-checking tool MCMAS which relies on the memoryless semantics for ATL with imperfect information\, and the problems that arise when implementing the model-checking algorithms for this case.
URL:https://sal.cs.unibuc.ro/event/the-frontier-between-decidability-and-undecidability-for-logics-for-strategic-reasoning-in-the-presence-of-imperfect-information/
LOCATION:Facultatea de Matematica si Informatica\, sala Google
CATEGORIES:Logic Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20181220T100000
DTEND;TZID=Europe/Bucharest:20181220T120000
DTSTAMP:20260620T150000
CREATED:20181217T151738Z
LAST-MODIFIED:20181217T151738Z
UID:268-1545300000-1545307200@sal.cs.unibuc.ro
SUMMARY:The finitary content of sunny nonexpansive retractions
DESCRIPTION:Andrei Sipoș (TU Darmstadt & IMAR). \n\nThe goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often\, such proofs make use of strong mathematical principles\, but a preliminary analysis may show that they are not actually needed\, so the proof may be carried out in a system of strength corresponding roughly to first-order arithmetic. Following a number of significant advances in this vein by Kohlenbach in 2011 and by Kohlenbach and Leuștean in 2012\, we now tackle a long-standing open question: the quantitative analysis of the strong convergence of resolvents in classes of Banach spaces more general than Hilbert spaces. \nThis result was proven for the class of uniformly smooth Banach spaces by Reich in 1980. What we do is to analyze a proof given in 1990 by Morales\, showing that adding the hypothesis of the space being uniformly convex\, and thus still covering the case of L^p spaces\, can serve to eliminate the strongest principles used in the proof by way of a modulus of convexity for the squared norm of such spaces. A further procedure of arithmetization brings the proof down to System T so the proper analysis may proceed. After obtaining a non-effective realizer of the metastability statement\, this is majorized in order to obtain the desired rate. Subsequent considerations calibrate this bound to T_1. It particular\, this result completes some analyses that had previously been obtained only partially\, yielding rates of metastability within the above-considered class of Banach spaces for the Halpern and Bruck iterations. \nThese results are joint work with Ulrich Kohlenbach. \n\nReferences:\n[1] U. Kohlenbach\, A. Sipoș\, The finitary content of sunny nonexpansive retractions. arXiv:1812.04940 [math.FA]\, 2018. Preprint. Up-to-date version at: https://www2.mathematik.tu-darmstadt.de/~kohlenbach/resolvent-paper.pdf
URL:https://sal.cs.unibuc.ro/event/the-finitary-content-of-sunny-nonexpansive-retractions/
LOCATION:Facultatea de Matematica si Informatica\, sala 202
CATEGORIES:Logic Seminar,Seminar
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Bucharest:20181206T100000
DTEND;TZID=Europe/Bucharest:20181206T120000
DTSTAMP:20260620T150000
CREATED:20181126T110006Z
LAST-MODIFIED:20181201T041129Z
UID:208-1544090400-1544097600@sal.cs.unibuc.ro
SUMMARY:Classical and quantum degrees of truth: a new look at the effects of a Hilbert space
DESCRIPTION:Speaker: Roberto Giuntini (University of Cagliari). \n\nWe investigate certain Brouwer-Zadeh lattices that serve as abstract counterparts of lattices of effects in Hilbert spaces under the spectral ordering. These algebras\, called PBZ∗-lattices\, can also be seen as generalisations of orthomodular lattices and are remarkable for the collapse of three notions of “sharpness” that are distinct in general Brouwer-Zadeh lattices. We investigate the structure theory of PBZ∗-lattices and their reducts; in particular\, we prove some embedding results for PBZ∗-lattices and provide an initial description of the lattice of PBZ∗-varieties.
URL:https://sal.cs.unibuc.ro/event/classical-and-quantum-degrees-of-truth-a-new-look-at-the-effects-of-a-hilbert-space/
LOCATION:Facultatea de Matematica si Informatica\, sala 202
CATEGORIES:Logic Seminar,Seminar
END:VEVENT
END:VCALENDAR