Supergroup BLAST!
Shay Logan
Supergroup Talk:
Speaker: Daniel Găină
Title: Forcing and Calculi for Hybrid Logics
Time and Date: Thursday, December 3rd, 19:00 GMT-6
Link: https://ksu.zoom.us/j/96608715294?pwd=elFFaVQ3Q0pwbzJScDZOWkhYRGlzdz09
Meeting ID: 966 0871 5294
Passcode: calculi
Abstract: The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems.
Talks by Member Groups:
Helsinki Logic Seminar
Speaker: Miika Hannula
Title: On the Complexity of Horn and Krom Fragments of Second-Order Boolean Logic
Time and Date: Wednesday, December 2nd 4:00 (GMT-6)
Link: https://us02web.zoom.us/j/4762106037?pwd=ckc1UzhDSHJmQ3I2bEpmNjNWcDNsZz09
Abstract: Dependency quantified Boolean formulae (DQBF) provide a canonical complete problem for non-deterministic exponential time. Restricted to Horn formulae this problem, then known as DQHORN, collapses to standard Horn satisfiability and is thus solvable in polynomial time. In this talk we isolate DQHORN as a fragment of second-order Boolean logic over CNF formulae with restrictions on clause and term structure. In particular, we consider whether some of the restrictions inherited from DQHORN can be loosened without increase in complexity. As a result, we obtain a complexity classification for various fragments of second-order Boolean logic.
Proof Theory Seminar
Speaker: Ulrich Kohlenbach
Title: Proof Mining and the "Lion-Man" game
Time and Date: Wednesday, December 2nd 11:00 (GMT-6)
Link: see https://www.proofsociety.org/proof-theory-seminar/participate.html
Colloquium LogicaeAbstract: 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 epsilon-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.
(Joint work with Genaro López-Acedo and Adriana Nicolae.)
Speaker: David Fuenmayor
Title: Generalized topological semantics for weak negations and applications to the analysis of Gödel's incompleteness theorem
Time and Date: Wednesday, December 2nd 13:00 (GMT-6)
Link: https://conferenciaweb.rnp.br/spaces/unicamp-cle-colloquium-logicae
Abstract: This talk is divided into two parts. First, I introduce a
sort of generalized topological semantics for paraconsistent and paracomplete (e.g. intuitionistic) logics by drawing upon early works on topological Boolean algebras (cf. Kuratowski, Zarycki, McKinsey & Tarski). In the second part, I present some preliminary joint work with Walter Carnielli [1] which formalizes the 'last mile' of the proof of Gödel's incompleteness theorem using some weak paraconsistent
Logics of Formal Inconsistency (a special case of the logics discussed in the first part). All presented results have been obtained with help of the proof assistant Isabelle/HOL. The idea is to motivate a (hopefully lively) discussion on the use of automated reasoning with non-classical logics in the formalization and (re)interpretation of influential meta-mathematical results.
[1] W. Carnielli, D. Fuenmayor (2020). Gödel blooming: the
incompleteness theorems from a paraconsistent perspective. Preprint. Vol. 19 No. 4 (2020) CLE e-prints
(https://www.cle.unicamp.br/eprints/index.php/CLE_e-Prints/issue/view/243)
Talk #1:
Speaker: Zoé Christoff (University of Groningen)
Title: Group Knowledge in Epistemic Logic with Names
Time and Date: Thursday, December 3rd 8:30 (GMT-6)
Abstract: In many situations, we refer to a group of agents using a label, say "Trump supporters" or "trolls", without knowing exactly who the members of the group are. Sometimes, we even fail to know whether we, ourselves, are members of a given group. Yet, epistemic logic typically comes with the simplifying assumption that group membership is common knowledge among the entire population. In 1993 already, Grove and Halpern introduced a generalized epistemic logic relaxing this assumption and replacing the usual indexes to denote agents with abstract names that can have different referents, both individuals or groups, in different possible worlds. In that generalized framework, they replace the standard K_i modalities with modalities of the form S_n and E_n, for "someone with name n knows" and "everyone with name n knows", respectively. In our current work, we discuss extensions of this generalized logic with group modalities for common knowledge and distributed knowledge.(joint work with Marta Bílková and Olivier Roy)
Reference: A. J. Grove and J. Y. Halpern. Naming and Identity in Epistemic Logics Part I: The Propositional Case. Journal of Logic and Computation, 3(4):345–378, 08, 1993
Talk #2:
Speaker: Aybüke Özgün (University of Amsterdam)
Title: Uncertainty about Evidence
Time and Date: Thursday, December 3rd 9:45 (GMT-6)
Abstract: We develop a logical framework for reasoning about knowledge and evidence in which the agent may be uncertain about how to interpret their evidence. Rather than representing an evidential state as a fixed subset of the state space, our models allow the set of possible worlds that a piece of evidence corresponds to to vary from one possible world to another, and therefore itself be the subject of uncertainty. Such structures can be viewed as (epistemically motivated) generalizations of topological spaces. In this context, there arises a natural distinction between what is actually entailed by the evidence and what the agent knows is entailed by the evidence---with the latter, in general, being much weaker. We provide a sound and complete axiomatization of the corresponding bi-modal logic of knowledge and evidence entailment, and investigate some natural extensions of this core system, including the addition of a belief modality and its interaction with evidence interpretation and entailment, and the addition of a “knowability" modality interpreted via a (generalized) interior operator.
This is joint work with Adam Bjorndahl.
Lógicos em Quarentena
Speaker: Stéphane Graham-Lengrand
Title: Realisability semantics of abstract focussing
Time and Date: Thursday, December 3rd 13:00 (GMT-6)
UConn Logic GroupAbstract: We present a sequent calculus for abstract focussing, as a highly parametric typing system for proof-terms. In the tradition of Zeilberger's work, logical connectives and their introduction rules are left as parameters, collapsing the synchronous and asynchronous phases of focussing as macro rules. Further parameterisation of context extension makes standard classical and intuitionistic focussed sequent calculi instances of the abstract one. We then define the realisability semantics of the system, on the basis of Munch-Maccagnoni's orthogonality models for the classical focussed sequent calculus, but now operating at the higher level of abstraction mentioned above. The Adequacy Lemma can be proved at that level: if a term is of type A, then its denotation in the realisability model is in the (set-theoretic) interpretation of A. The proof explicitly connects two forms of universal quantification: on the semantic side, the universal quantification involved when taking the orthogonal of a set; and on the syntactic side, the universal quantification involved in the macro rule for the asynchronous phase. The system and its semantics are all formalised in Coq.
Speaker: Nadine Theiler
Title: An Epistemic Bridge for Presupposition Projection in Questions
Time and Date: Friday, December 4th 13:00 (GMT-6)
Meeting ID: 871 4533 4762
Passcode: presup
Abstract: Semantic presuppositions are certain inferences associated with words or linguistic constructions. For example, if someone tells you that they “recently started doing yoga”, then this presupposes that they didn’t do yoga before.
A problem that has occupied semanticists for decades is how the presuppositions of a complex sentence can be computed from the presuppositions of its parts. Another way of putting this problem is, how do presuppositions project in various environments?
In this talk, I will discuss presupposition projection in one particular linguistic environment, namely in questions, arguing that it should be treated pragmatically. I will motivate a generalized version of Stalnaker’s bridge principle and show that it makes correct predictions for a range of different interrogative forms and different question uses.
Other Notes and Announcements:
To access the supergroup calendar, please follow this link: https://calendar.google.com/calendar?cid=ZGhoanNoanF1bGhmaG9xam5scDJlc2o0bDhAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbQ
To access the member groups joint calendar, please follow this link: https://calendar.google.com/calendar?cid=aG8wNWljaGxkNXI2N2oyMnZvY3BzdmRoMWNAZ3JvdXAuY2FsZW5kYXIuZ29vZ2xlLmNvbQ
If you represent a member group and would like your events to appear on the joint calendar, be sure to add them! Contact any of the organizers if you need permission to do so.
Yay for logic!
Shay Logan
Itala Maria Loffredo D'Ottaviano
--
Você recebeu essa mensagem porque está inscrito no grupo "LOGICA-L" dos Grupos do Google.
Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+u...@dimap.ufrn.br.
Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMTR9906ofqJzLyQpk0A996_%3D6Eyhh1Ffk%3D5XE-D-%3DVPW167eA%40mail.gmail.com.
--