17:00-17:30 - Ana Cruz

17:30-18:00 - Leandro Gomes

18:00-18:30 - Alfredo Freire

(joint work with Alexandre Madeira and Luís Soares Barbosa)

Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. In this kind of scenarios, arising e.g. in knowledge representation, simulation of biological systems, or quantum computation, inconsistency has to be addressed in a precise and controlled way. In this presentation we generalises Belnap-Dunn four-valued logic, introducing paraconsistent transition systems (PTS), endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values, and their modal logic. The material presented in this talk was recently published in [CMB22].

**References: **

[CMB22]A logic for paraconsistent transition systems A. Cruz, A. Madeira and L. Barbosa. Non-Classic Logics. Theory and Applications. EPTCS (in print)

(joint work with Alexandre Madeira and Luís Soares Barbosa)

This work presents a framework to formally reason about weighted compu- tations or, more precisely, programs and assertions about them whose execution or evaluation has some form of weight associated. By weight we mean a value which may represent, for example, an uncertainty in the execution, or a quan- tity of resources consumed, such as energy or time. Examples of such systems range from device-to-device communications, network biological processes, clin- ical decision support systems or robot control, having become ubiquitous in our everyday life in the past years. Due to the complexity underlying the introduc- tion of these parameters, software engineering is forced to call upon rigorous development methodologies which provide a high assurance of each software product. And if it is true that the development, analysis and verification of these systems are increasingly laid on this exactly approach, the current pro- gramming practices are not capable to offer a framework which is, at the same time, generic enough to capture such paradigms, and able to satisfy the specific requirements for each application domain.
We intend to address this challenge by presenting a methodology for the systematic development of semantics and logics to reason about two distinct classes of programs. In the first class, that we call single-flow computation, each execution is a single transition with an associated weight. In the second class, that we call multi-flow computation, each execution may assume multi- ple simultaneous execution paths, each one of them with a, possible distinct, weight. In this work we define, for each class of computation, a semantics, and we prove that it forms a suitable algebra to reason about programs of that class. For that end, we define operators which interpret the basic constructions of an imperative programming language: sequential composition, conditionals and iteration. From here we construct (a family of) dynamic logics, including the respective axiomatic system, allowing to verify properties over those programs.
For single-flow computations, we define as well a notion of bisimilarity on the models of the generated logics, and prove the modal invariance property for those logics.

**References: **

[Koz97] Dexter Kozen. Kleene algebra with tests. ACM Transactions on Pro- gramming Languages and Systems, 19(3):427–443, 1997.

[Gog67] J.A Goguen. L-fuzzy sets. Journal of Mathematical Analysis and Applications, 18(1):145 – 174, 1967.

[MNM16] Alexandre Madeira, Renato Neves, and Manuel A. Martins. An ex- ercise on the generation of many-valued dynamic logics. Journal of Logical and Algebraic Methods in Programming, 85(5):1011–1037, 2016.

[FKST17] Hitoshi Furusawa, Yasuo Kawahara, Georg Struth, and Norihiro Tsumagari. Kleisli, Parikh and Peleg compositions and liftings for multirela- tions. Journal of Logical and Algebraic Methods in Programming, 90:84–101, 2017.

[VMA10] Thom as Vetterlein, Harald Mandl, and Klaus-Peter Adlassnig. Fuzzy Arden syntax: A fuzzy programming language for medicine. Artificial Intel- ligence in Medicine, 49(1):1 – 10, 2010.

(joint work with Manuel A. Martins)

In this presentation, we deal with the problem of putting together modal worlds/or states that operate in different logic systems. An important concern we should address is whether or not it makes sense to evaluate the possibility of a statement in a world w by inspecting its truth value in a world w in a alternative logic. We will introduce a modal notion and structure that accommodate communication between logic systems by fixing a common lattice L where different logics build their semantics (i.e. the semantics of each logic being considered is a sublattice of L). In this system, necessity and possibility of a statement should not solely rely on the satisfaction relation in each world and the accessibility relation. The value of a formula φ will be defined in terms of a comparison between the values of φ in accessible worlds and the common lattice L. We investigate general properties for many logic modal structures. For instance, we will determine conditions over the lattice L and/or sublattice of an specific world that imply validity of the axiom K and/or the rule of necessitation. We will also investigate natural conditions where formulas φ can be said to be necessary/possible even though an/all accessible world/s falsify φ. Finally, we will discuss frames that characterize dynamic relations between logic systems (classically increasing, classically decreasing and dialectic frames).

**References: **

[BJ19] Francesco Berto and Mark Jago. Impossible worlds. Oxford University Press, 2019.

[CWJ19] Petr Cintula, Z Weber, and S Ju. “Editors’ introduction: Special issue on non-classical modal and predicate logics”. In: Logic Journal of the IGPL 27.4 (May 2019), pp. 385–386.

[Kri72] Saul A. Kripke. “Naming and Necessity”. In: Semantics of Natural Language. Ed. by Donald Davidson and Gilbert Harman. Dordrecht: Springer Netherlands, 1972, pp. 253–355.

[Pri08] Graham Priest. An introduction to non-classical logic: From if to is. Cambridge University Press, 2008.

[Qui86] Willard V Quine. Philosophy of logic. Harvard University Press, 1986.

Alexandre Madeira