The Encontro Brasileiro de Lógica (Brazilian Logic Meeting) is one of the most traditional academic events in Latin America, occurring approximately every two years in different cities across Brazil since 1979. In the last decades, the meeting has been gathering more than a hundred logicians from many parts of the world, meaning it welcomes people from many cultural and scientific backgrounds ranging from Philosophy to Computer Science. The week-long event is usually preceded by a Logic School aiming to qualify the logical education of undergraduate and graduate students. The EBL is a dynamic blend of plenary and parallel sessions, offering participants a rich and immersive experience that fosters knowledge exchange and interdisciplinary collaboration. The twentieth edition of the Encontro Brasileiro de Lógica (XX EBL) was held from 12 to 16 Spetember 2022, at the Institute of Mathematics and Statistics of the Universidade Federal da Bahia, in the beautiful city of Salvador da Bahia—one of the oldest Brazilian cities and the first capital of the nation. The meeting was initially expected to take place in 2021, but due to the COVID-19 pandemic, the Brazilian Logic Society postponed it to the subsequent year.

Insulin synthesis is a complex and essential biological process involving a series of interconnected subprocesses. We present a model of the translational process and post-translational modifications occurring in insulin biosynthesis. Using Colored Petri Nets (CPNs), we accurately represent sets of interactions among components such as amino acids, polypeptide chains, and other cellular compounds. This CPN framework captures the intricate state changes within biological processes and establishes a theoretical foundation for modeling and analyzing other critical biological processes.

Abstract Hoare Logic has a long tradition in formal verification and has been continuously developed and used to verify a broad class of programs, including sequential, object-oriented, and concurrent programs. Here we focus on partial and total correctness assertions within the framework of Hoare logic and show that a comprehensive categorical analysis of its axiomatic semantics needs the languages of indexed and fibered category theory. We consider Hoare formulas with local, finite contexts, of program and logical variables. The structural features of Hoare assertions are presented in an indexed setting, while the logical features of deduction are modeled in the fibered one.

Petri Nets are a widely used formalism to deal with concurrent systems. Dynamic Logics (DLs) are a family of modal logics where each modality corresponds to a program. Petri-PDL is a logical language that combines these two approaches: it is a dynamic logic where programs are replaced by Petri Nets. In this work we present a clausal resolution-based calculus for Petri-PDL. Given a Petri-PDL formula, we show how to obtain its translation into a normal form to which a set of resolution-based inference rules are applied. We show that the resulting calculus is sound, complete, and terminating. Some examples of the application of the method are also given.

Céu is a synchronous programming language for embedded soft real-time systems. It focuses on control-flow safety features, such as safe shared-memory concurrency and safe abortion of lines of execution, while enforcing memory bounded, deterministic, and terminating reactions to the environment. In this work, we present a small-step structural operational semantics for Céu and a proof that reactions have the properties enumerated above: that for a given arbitrary timeline of input events, multiple executions of the same program always react in bounded time and arrive at the same final finite memory state.

In Brazil, all legal professionals must demonstrate their knowledge of the law and its application by passing the OAB exams, the national Bar exams. This article describes the construction of a new data set and some preliminary experiments on it, treating the problem of finding the justification for the answers to questions. The results provide a baseline performance measure against which to evaluate future improvements. We discuss the reasons to the poor performance and propose next steps.

K-mer Mapping, an internal process for many de novo genome fragments assembly methods, constitutes a computational challenge due to its high main memory consumption. We present in this paper a study of indexing methods to deal with this problem, considering plant genome assembling. We propose an ad-hoc I/O cost model to analyze the performance of B+- tree and hashing index structures. We use indexes to detect duplicate k-mers and improve the execution time. An actual RDBMS implementation for experiments with a sugarcane data set shows that one can obtain considerable performance gains while reducing RAM requirements.

Journal Article Towards a uniform presentation of logical systems by indexed categories and adjoint situations Get access U. Wolter, U. Wolter Department of Informatics, University of Bergen, Norway.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar A. Martini, A. Martini Faculdade de Informática, PUCRS, Brasil.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar E. H. Häusler E. H. Häusler Departamento de Ciência da Computação, PUC-Rio, Brasil.E-mail: [email protected] Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 25, Issue 1, February 2015, Pages 57–93, https://doi.org/10.1093/logcom/exs038 Published: 03 September 2012 Article history Received: 26 January 2012 Published: 03 September 2012

We present a means of generating a mobile clientserver application that enables customized remote monitoring of patients with chronic diseases. The customization is based on parameters and formal descriptions of: type of chronic disease, patient preferences, the monitoring procedure required by the doctor, prescribed medication and information about the current context (i.e., environment) of the patient, obtained from sensors. Based on this, the system determines which pieces of information should be regularly obtained from the patient through questionnaires and/or sensors of the smart phone and sensors connected to it. Relevant information are the ones that help to detect possible changes in the patient's health condition and the monitoring process of a patient by the doctor. The medical treatment and the kind of chronic disease will define the set of data to be collected. It should be stressed that the goal is not to support automatic medical diagnosis, but only to provide means for physicians to obtain updated information about their patients, so as to allow remote monitoring of patients.

This paper briefly shows how Intuitionistic Description Logic can be considered a good alternative to classical ALC as far as formalizing legal knowledge is concerned.

This paper considers a formal framework to contextualize ontologies and presents a formal algebra to manipulate these entities providing several ways of composing ontologies, contexts or both. The algebra gives the flexibility that is required to model applications where the meaning of an entity depends on environment constraints or where dynamic changes in the environment must be considered.