BEGIN:VCALENDAR VERSION:2.0 PRODID:-//SECURITY & APPLIED LOGIC - ECPv6.15.20//NONSGML v1.0//EN CALSCALE:GREGORIAN METHOD:PUBLISH X-WR-CALNAME:SECURITY & APPLIED LOGIC 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: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 BEGIN:DAYLIGHT TZOFFSETFROM:+0200 TZOFFSETTO:+0300 TZNAME:EEST DTSTART:20200329T010000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0300 TZOFFSETTO:+0200 TZNAME:EET DTSTART:20201025T010000 END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0200 TZOFFSETTO:+0300 TZNAME:EEST DTSTART:20210328T010000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0300 TZOFFSETTO:+0200 TZNAME:EET DTSTART:20211031T010000 END:STANDARD BEGIN:DAYLIGHT TZOFFSETFROM:+0200 TZOFFSETTO:+0300 TZNAME:EEST DTSTART:20220327T010000 END:DAYLIGHT BEGIN:STANDARD TZOFFSETFROM:+0300 TZOFFSETTO:+0200 TZNAME:EET DTSTART:20221030T010000 END:STANDARD END:VTIMEZONE BEGIN:VTIMEZONE TZID:UTC BEGIN:STANDARD TZOFFSETFROM:+0000 TZOFFSETTO:+0000 TZNAME:UTC DTSTART:20180101T000000 END:STANDARD END:VTIMEZONE BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210422T100000 DTEND;TZID=Europe/Bucharest:20210422T120000 DTSTAMP:20260620T133438 CREATED:20210421T165207Z LAST-MODIFIED:20210421T165207Z UID:706-1619085600-1619092800@sal.cs.unibuc.ro SUMMARY:Kernelization\, Proof Complexity and Social Choice DESCRIPTION:Title: Kernelization\, Proof Complexity and Social Choice \nSpeaker: Gabriel Istrate (West University of Timișoara) \n\nAbstract: \n\nWe display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically\, we show that the existence of data reduction rules for a parameterized problem having (a) a small-length reduction chain\, and (b) small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015)\, we show that propositional formulas expressing (a stronger form of) the Kneser-Lovasz Theorem have polynomial size Frege proofs for each constant value of the parameter k. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lovasz Theorem). Another notable application of our framework is to impossibility results in computational social choice: we show that\, for any fixed number of agents\, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs. \nThis is joint work with Cosmin Bonchiș and Adrian Crăciun. URL:https://sal.cs.unibuc.ro/event/kernelization-proof-complexity-and-social-choice/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210401T100000 DTEND;TZID=Europe/Bucharest:20210401T120000 DTSTAMP:20260620T133438 CREATED:20210329T200608Z LAST-MODIFIED:20210329T200608Z UID:701-1617271200-1617278400@sal.cs.unibuc.ro SUMMARY:An Introduction to Protocols in Dynamic Epistemic Logic DESCRIPTION:Title: An Introduction to Protocols in Dynamic Epistemic Logic \nSpeaker: Alexandru Dragomir (University of Bucharest) \n\nAbstract: \nDynamic epistemic logics are useful in reasoning about knowledge and acts of learning\, seen as epistemic actions. However\, not all epistemic actions are allowed to be executed in an initial epistemic model\, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: Hoshi’s [1]\, and Wang’s [2]. \n\nReferences: \n[1] T. Hoshi\, Epistemic dynamics and protocol information. PhD thesis\, Stanford\, CA\, USA\, 2009.\n[2] Y. Wang\, Epistemic Modelling and Protocol Dynamics. PhD thesis\, University of Amsterdam\, 2010. URL:https://sal.cs.unibuc.ro/event/an-introduction-to-protocols-in-dynamic-epistemic-logic/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210325T100000 DTEND;TZID=Europe/Bucharest:20210325T120000 DTSTAMP:20260620T133438 CREATED:20210322T160836Z LAST-MODIFIED:20210323T090618Z UID:697-1616666400-1616673600@sal.cs.unibuc.ro SUMMARY:Regular matching problems for infinite trees DESCRIPTION:Title: Regular matching problems for infinite trees \nSpeaker: Mircea Marin (West University of Timișoara) \n\nAbstract: \nWe study the matching problem “∃σ:σ(L)⊆R?” where L and R are regular tree languages over finite ranked alphabets X and Σ respectively\, and σ is a substitution such that σ(x) is a set of trees in T(Σ∪H)∖H for all x∈X. Here\, H denotes a set of holes which are used to define a concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook Regular algebra and finite machines and showed that if L and R are regular\, then the problem “∃σ:∀x∈X:σ(x)≠∅∧σ(L)⊆R?” is decidable. Moreover\, there are only finitely many maximal solutions\, which are regular and effectively computable. We extend Conway’s results when L and R are regular languages of finite and infinite trees\, and language substitution is applied inside-out. We show that if L⊆T(X) and R⊆T(Σ) are regular tree languages then the problem “∃σ∀x∈X:σ(x)≠∅∧σio(L)⊆R?” is decidable. Moreover\, there are only finitely many maximal solutions\, which are regular and effectively computable. The corresponding question for the outside-in extension σoi remains open\, even in the restricted setting of finite trees. Our main result is the decidability of “∃σ:σio(L)⊆R?” if R is regular and L belongs to a class of tree languages closed under intersection with regular sets. Such a special case pops up if L is context-free.\nThis is joint work with Carlos Camino\, Volker Diekert\, Besik Dundua and Géraud Sénizergues. \n\nReferences: \n[1] C. Camino\, V. Diekert\, B. Dundua\, M. Marin\, G. Sénizergues\, Regular matching problems for infinite trees. arXiv:2004.09926 [cs.FL]\, 2021. URL:https://sal.cs.unibuc.ro/event/regular-matching-problems-for-infinite-trees/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210318T100000 DTEND;TZID=Europe/Bucharest:20210318T120000 DTSTAMP:20260620T133438 CREATED:20210317T151527Z LAST-MODIFIED:20210317T204833Z UID:681-1616061600-1616068800@sal.cs.unibuc.ro SUMMARY:A proof mining case study on the unit interval DESCRIPTION:Title: A proof mining case study on the unit interval \nSpeaker: Andrei Sipoș (University of Bucharest & IMAR) \n\nAbstract:  \n\nIn 1991\, Borwein and Borwein proved [1] the following: if L>0\, f : [0\,1] → [0\,1] is L-Lipschitz\, (xn)\, (tn) ⊆ [0\,1] are such that for all n\, xn+1=(1-tn)xn+tnf(xn) and there is a δ>0 such that for all n\, tn≤(2-δ)/(L+1)\, then the sequence (xn) converges.\nThe relevant fact here is that the main argument used in their proof is of a kind that hasn’t been analyzed yet from the point of view of proof mining\, and thus it may serve as an illustrative new case study. We shall present our work [2] on the proof\, showing how to extract a uniform and computable rate of metastability for the above family of sequences.\nReferences: \n\n\n[1] D. Borwein\, J. Borwein\, Fixed point iterations for real functions. J. Math. Anal. Appl. 157\, no. 1\, 112–126\, 1991.\n[2] A. Sipoș\, Rates of metastability for iterations on the unit interval. arXiv:2008.03934 [math.CA]\, 2020. URL:https://sal.cs.unibuc.ro/event/a-proof-mining-case-study-on-the-unit-interval/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210311T100000 DTEND;TZID=Europe/Bucharest:20210311T120000 DTSTAMP:20260620T133438 CREATED:20210310T154158Z LAST-MODIFIED:20210317T154308Z UID:683-1615456800-1615464000@sal.cs.unibuc.ro SUMMARY:Exponential Diophantine equations over ℚ  DESCRIPTION:Title:  Exponential Diophantine equations over ℚ \nSpeaker: Mihai Prunescu (University of Bucharest & IMAR) \n\nAbstract: \n\nIn a previous exposition [1] we have seen that the solvability over ℚ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable\, and that this happens as well for some narrower families of exponential Diophantine equations. \nReferences: \n\n[1] M. Prunescu\, The exponential Diophantine problem for ℚ. The Journal of Symbolic Logic\, Volume 85\, Issue 2\, 671–672\, 2020. URL:https://sal.cs.unibuc.ro/event/exponential-diophantine-equations-over-%e2%84%9a/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210304T100000 DTEND;TZID=Europe/Bucharest:20210304T120000 DTSTAMP:20260620T133438 CREATED:20210303T165215Z LAST-MODIFIED:20210317T165240Z UID:691-1614852000-1614859200@sal.cs.unibuc.ro SUMMARY:Unwinding of proofs DESCRIPTION:Title: Unwinding of proofs \nSpeaker: Pedro Pinto (TU Darmstadt) \n\nAbstract: \nThe unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: “What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?”\n \n \nThis research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1\,2]. Through the use of proof-theoretical tools\, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles.\n\nIn this talk\, we set out to give a brief introduction to the proof mining program\, focusing on the following points: \n\n\n\nfunctional interpretations in an introductory way;\nthe bounded functional interpretation [3\,4];\na concrete translation example: the metric projection argument.\n\nWe finish with a brief discussion of some recent results [5\,6]. \nReferences: \n\n[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg\, 2008.\n[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov\, P. Ney de Souza\, editor\, Proceedings of the International Congress of Mathematicians – Rio de Janeiro 2018\, Vol. II: Invited lectures\, pages 61–82. World Sci. Publ.\, Hackensack\, NJ\, 2019.\n[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic\, 135:73-112\, 2005.\n[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic\, 157:122-129\, 2009.\n[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA]\, 2021.\n[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA]\, 2021.\n  \n\n  \nReferences: URL:https://sal.cs.unibuc.ro/event/unwinding-of-proofs/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20210225T100000 DTEND;TZID=Europe/Bucharest:20210225T120000 DTSTAMP:20260620T133438 CREATED:20210224T154805Z LAST-MODIFIED:20210317T164757Z UID:687-1614247200-1614254400@sal.cs.unibuc.ro SUMMARY:Formalizing Gödel's System T in Lean DESCRIPTION:Title: Formalizing Gödel’s System T in Lean \nSpeaker: Horațiu Cheval (University of Bucharest) \n\nAbstract: \n\nIn 1958\, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory\, notably the program of proof mining. We give a brief overview of Gödel’s System T and then explore a formalization thereof as a deep embedding in the Lean proof assistant. \nReferences: \n\n[1] mathlib Community\, The Lean Mathematical Library\, 2019. URL:https://sal.cs.unibuc.ro/event/formalizing-go%cc%88dels-system-t-in-lean/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20200312T100000 DTEND;TZID=Europe/Bucharest:20200312T120000 DTSTAMP:20260620T133438 CREATED:20200309T110155Z LAST-MODIFIED:20200311T122705Z UID:588-1584007200-1584014400@sal.cs.unibuc.ro SUMMARY:POSTPONED: Protocols in Dynamic Epistemic Logic DESCRIPTION:POSTPONED UNTIL FURTHER NOTICE.\n\nSpeaker: Alexandru Dragomir (University of Bucharest)\n\nTitle: Protocols in Dynamic Epistemic Logic\nAbstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (epistemic actions). However\, not all epistemic actions are allowed to be executed in an initial epistemic model\, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to the account of protocols in [1\, 2]. \n\n\nReferences:\n[1] H. van Ditmarsch\, S. Ghosh\, R. Verbrugge\, Y. Wang\, Hidden protocols: Modifying our expectations in an evolving world\, Artificial Intelligence 208 (2014)\, 18-40.\n[2] Y. Wang\, Epistemic Modelling and Protocol Dynamics\, PhD thesis\, University of Amsterdam\, 2010. URL:https://sal.cs.unibuc.ro/event/protocols-in-dynamic-epistemic-logic-2/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=Europe/Bucharest:20200227T100000 DTEND;TZID=Europe/Bucharest:20200227T120000 DTSTAMP:20260620T133438 CREATED:20200309T105935Z LAST-MODIFIED:20200309T110749Z UID:585-1582797600-1582804800@sal.cs.unibuc.ro SUMMARY:A quantitative analysis of the “Lion-Man” game DESCRIPTION:Speaker: Ulrich Kohlenbach (Technische Universität Darmstadt)\nTitle: A quantitative analysis of the “Lion-Man” game\nAbstract: We analyze\, based on an interplay between ideas and techniques from logic and geometric analysis\, a pursuit-evasion game. More precisely\, we focus on a discrete lion and man game with an ε-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and\, using ideas stemming from proof mining\, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis\, we study the relation among different convexity properties in the setting of geodesic spaces.\nJoint work with Genaro López-Acedo and Adriana Nicolae. \n\n\nReferences:\n[1] U. Kohlenbach\, G. López-Acedo\, A. Nicolae\, A quantitative analysis of the “Lion-Man” game. arXiv:1806.04496 [math.MG]\, 2019. Submitted. URL:https://sal.cs.unibuc.ro/event/a-quantitative-analysis-of-the-lion-man-game/ LOCATION:Facultatea de Matematica si Informatica\, sala Google CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20191219T100000 DTEND;TZID=UTC:20191219T120000 DTSTAMP:20260620T133438 CREATED:20191217T061235Z LAST-MODIFIED:20191217T061235Z UID:548-1576749600-1576756800@sal.cs.unibuc.ro SUMMARY:First-order logic and vagueness DESCRIPTION:Speaker: Marian Calborean (University of Bucharest) \n\nAbstract: The Sorites paradox is usually studied as a propositional paradox. However\, the general form of the Sorites is second-order\, with three main features. It doesn’t contain any arbitrary parameters. It can be used to generate the propositional Sorites by appropriate replacement of the second-order premise with arbitrary clauses. Finally\, it is generally nonfirstorderizable\, relying on the notion of transitive closure of a relation. However\, it can be expressed in FOL with a finite upper bound on the elements of the relation. This leads to a definition of vagueness in classical FOL\, using the interplay between a total preorder and a monadic predicate. A notational extension of FOL will introduce a vague structure formed by the predicate (e.g.tall)\, the broad predicate (e.g. broadly tall) and the strict predicate (e.g. strictly tall). It allows the failure of a weak non-contradiction (e.g. ‘Some men are both broadly tall and broadly short’)\, the failure of a weak LEM (e.g. ‘Some men are neither strictly tall nor strictly short`)\, and the truth of a non-paradoxical tolerance (e.g. ‘If a person of n cm is strictly tall\, a person of n-1 cm is broadly tall’). \nReferences:\n[1] P. Cobreros\, P. Egré\, D. Ripley\, R\, Van Rooij\, Tolerant\, Classical\, Strict\, Journal of Philosophical Logic 41 (2019)\, 347-385.\n[2] D. Graff\, Shifting Sands: An Interest-Relative Theory of Vagueness\, Philosophical Topics 28 (2000)\, 45-81.\n[3] U. Keller\, Some remarks on the definability of transitive closure in first-order logic and Datalog\, Internal report\, Digital Enterprise Research Institute (DERI)\, University of Innsbruck\, 2004.\n[4] K.G. Lucey\, he ancestral relation without classes\, Notre Dame Journal of Formal Logic 20 (1979)\, 281-284. URL:https://sal.cs.unibuc.ro/event/first-order-logic-and-vagueness/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20191212T100000 DTEND;TZID=UTC:20191212T120000 DTSTAMP:20260620T133438 CREATED:20191125T084235Z LAST-MODIFIED:20191211T053426Z UID:524-1576144800-1576152000@sal.cs.unibuc.ro SUMMARY:Operational Semantics of Security Protocols II DESCRIPTION:Speaker: Ioana Leustean (University of Bucharest) \n\nAbstract:  We continue our presentation on operational semantics of  security protocols\, as developed in: \nC. Cremers\, S. Mauw\, Operational Semantics and Verification of Security Protocols\, Springer\, 2012. URL:https://sal.cs.unibuc.ro/event/524/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20191121T100000 DTEND;TZID=UTC:20191121T120000 DTSTAMP:20260620T133438 CREATED:20191118T114517Z LAST-MODIFIED:20191211T053442Z UID:521-1574330400-1574337600@sal.cs.unibuc.ro SUMMARY:Operational Semantics of Security Protocols DESCRIPTION:Speaker:  Ioana Leustean (University of Bucharest) \n\nAbstract: After a brief overview of the formal methods used for analyzing security protocols\, we will focus on the operational semantics developed in: \nC. Cremers\, S. Mauw\, Operational Semantics and Verification of Security Protocols\, Springer\, 2012. \n  URL:https://sal.cs.unibuc.ro/event/operational-semantics-of-security-protocols/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20191101T093000 DTEND;TZID=UTC:20191103T130000 DTSTAMP:20260620T133438 CREATED:20191031T062011Z LAST-MODIFIED:20191031T062011Z UID:516-1572600600-1572786000@sal.cs.unibuc.ro SUMMARY:ManyVal 2019 DESCRIPTION:In perioada 1-3 noiembrie organizam workshop-ul international ManyVal 2019\, dedicat in special cercetarilor in logica cu mai multe valori. Editia actuala beneficiaza si de participarea unor filozofi-logicieni de marca. Pentru mai multe detalii puteti consulta pagina manifestarii:\n\n\n\n\n\nhttps://cs.unibuc.ro/events/manyval2019/\n\n\n\n\n\nPersoanele inregistrate vor primi kit-ul workshop-ului si vor putea participa la mesele si activitatile sociale anuntate.\n\n\n\n\n\nParticiparea la prezentari NU presupune plata taxei de inregistrare\, iar anumite materiale (program\, carte de abstracte) vor putea fi descarcate de pe pagina ManyVal 2019. URL:https://sal.cs.unibuc.ro/event/manyval-2019/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20191024T100000 DTEND;TZID=UTC:20191024T120000 DTSTAMP:20260620T133438 CREATED:20191021T122914Z LAST-MODIFIED:20191027T090711Z UID:510-1571911200-1571918400@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 [1]. BAN logic is 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. \nReferences:\n[1] M. Burrows\, M. Abadi\, R. Needham\, A logic of authentication. Proc. Roy. Soc. London Ser. A 426\, no. 1871\, 233–271\, 1989. URL:https://sal.cs.unibuc.ro/event/an-introduction-to-ban-logic-a-logic-of-authentication-2/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190919T100000 DTEND;TZID=UTC:20190919T120000 DTSTAMP:20260620T133438 CREATED:20190918T215721Z LAST-MODIFIED:20190918T215721Z UID:449-1568887200-1568894400@sal.cs.unibuc.ro SUMMARY:Local Reasoning about Parametric and Reconfigurable Component-based Systems DESCRIPTION:Speaker: Radu Iosif (CNRS – VERIMAG\, France) \n\nAbstract: We introduce a logical framework for the specification and verification of component-based systems\, in which finitely many component instances are active\, but the bound on their number is not known. Besides specifying and verifying parametric systems\, we consider the aspect of dynamic reconfiguration\, in which components can migrate at runtime on a physical map\, whose shape and size may change. We describe such para- metric and reconfigurable architectures using resource logics\, close in spirit to Separation Logic\, used to reason about dynamic pointer structures. These logics support the principle of local reasoning\, which is the key for writing modular specifications and building scalable verification algorithms\, that deal with large industrial-size systems. Joint work with Marius Bozga and Joseph Sifakis. URL:https://sal.cs.unibuc.ro/event/local-reasoning-about-parametric-and-reconfigurable-component-based-systems/ LOCATION:Facultatea de Matematica si Informatica\, sala Google CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190530T100000 DTEND;TZID=UTC:20190530T120000 DTSTAMP:20260620T133438 CREATED:20190529T063857Z LAST-MODIFIED:20190529T063857Z UID:421-1559210400-1559217600@sal.cs.unibuc.ro SUMMARY:Protocols in Dynamic Epistemic Logic DESCRIPTION:Speaker:  Alexandru Dragomir (University of Bucharest) \n\nAbstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (epistemic actions). However\, not all epistemic actions are allowed to be executed in an initial epistemic model\, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: one based on [1]\, and the second on [2]. \nReferences:\n[1] T. Hoshi\, Epistemic dynamics and protocol information\, PhD thesis\, Stanford University\, 2009.\n[2] Y. Wang\, Y. Epistemic Modelling and Protocol Dynamics\, PhD thesis\, University of Amsterdam\, 2010. URL:https://sal.cs.unibuc.ro/event/protocols-in-dynamic-epistemic-logic/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190516T100000 DTEND;TZID=UTC:20190516T120000 DTSTAMP:20260620T133438 CREATED:20190506T043334Z LAST-MODIFIED:20190514T093157Z UID:406-1558000800-1558008000@sal.cs.unibuc.ro SUMMARY:An introduction to hybrid-dynamic first-order logic DESCRIPTION:Speaker: Ionuţ Ţuţu (Royal Holloway\, University of London) \n\nAbstract: We propose a hybrid-dynamic first-order logic as a formal\nfoundation for specifying and reasoning about reconfigurable\nsystems. As the name suggests\, the formalism we develop extends\n(many-sorted) first-order logic with features that are common to\nhybrid and to dynamic logics. This provides certain key advantages for\ndealing with reconfiguration\, such as: (a) a signature of nominals\,\nincluding operation and relation symbols\, that allows references to\nspecific possible worlds / system configurations – as in the case of\nhybrid logics; (b) distinguished signatures of rigid and flexible\nsymbols\, where the rigid symbols are interpreted uniformly across\npossible worlds – this supports a rigid form of quantification\, which\nensures that variables have the same interpretation regardless of the\npossible world where they are evaluated; (c) hybrid terms\, which\nincrease the expressive power of the logic in the context of rigid\nsymbols; and (d) modal operators over dynamic-logic actions\, which are\ndefined as regular expressions over binary nominal relations. In this\ncontext\, we advance a notion of hybrid-dynamic Horn clause and develop\na series of results that lead to an initial-semantics theorem for the\nHorn-clause fragment of hybrid-dynamic first-order logic. URL:https://sal.cs.unibuc.ro/event/good-for-a-conclusion-not-good-enough-for-a-premise-natural-language-reasoning-and-the-logic-of-vagueness/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190411T100000 DTEND;TZID=UTC:20190411T120000 DTSTAMP:20260620T133438 CREATED:20190409T102018Z LAST-MODIFIED:20190409T102018Z UID:397-1554976800-1554984000@sal.cs.unibuc.ro SUMMARY:Around Hilbert's Tenth Problem DESCRIPTION:Speaker: Mihai Prunescu (University of Bucharest) \n\nAbstract: We discuss different implications of the negative answer of Hilbert’s Tenth Problem: the exponential Diophantine equation over ℕ and ℚ\, the minimal number of variables which lead to an undecidable problem over ℤ\, the homogeneous Diophantine problem over ℤ. URL:https://sal.cs.unibuc.ro/event/around-hilberts-tenth-problem/ CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190328T100000 DTEND;TZID=UTC:20190328T120000 DTSTAMP:20260620T133438 CREATED:20190325T165404Z LAST-MODIFIED:20190325T165404Z UID:391-1553767200-1553774400@sal.cs.unibuc.ro SUMMARY:Lindström's Theorems II DESCRIPTION:Speaker: Mihai Prunescu (University of Bucharest) \n\nAbstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms. \nReferences:\n[1] H.-D. Ebbinghaus\, J. Flum\, W. Thomas\, Mathematical Logic. Second edition\, Undergraduate Texts in Mathematics\, Springer\, 1996. URL:https://sal.cs.unibuc.ro/event/lindstroms-theorems-ii/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190314T100000 DTEND;TZID=UTC:20190314T100000 DTSTAMP:20260620T133438 CREATED:20190311T055525Z LAST-MODIFIED:20190311T055525Z UID:376-1552557600-1552557600@sal.cs.unibuc.ro SUMMARY:Lindström's Theorems DESCRIPTION:Speaker: Mihai Prunescu (University of Bucharest) \n\nAbstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms. \nReferences:\n[1] H.-D. Ebbinghaus\, J. Flum\, W. Thomas\, Mathematical Logic. Second edition\, Undergraduate Texts in Mathematics\, Springer\, 1996. URL:https://sal.cs.unibuc.ro/event/lindstroms-theorems/ LOCATION:Facultatea de Matematica si Informatica\, sala 202 CATEGORIES:Logic Seminar END:VEVENT BEGIN:VEVENT DTSTART;TZID=UTC:20190228T100000 DTEND;TZID=UTC:20190228T120000 DTSTAMP:20260620T133438 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:20260620T133438 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:20260620T133438 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:20260620T133438 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:20260620T133438 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