Given the increasing importance of security protocols in our daily activities and communication via internet, the efforts to develop mechanisms and models for verification of such protocols are always relevant. In this work, we explore the Dolev-Yao Multi-Agent Epistemic Logic by providing a tableaux method for it. This logic is an extension of Multi-Agent Epistemic Logic, aimed to verify authenticity and safety in communication protocols and inspired by the Dolev-Yao model, a seminal work in formal cryptography.
A teoria de revisão de crença AGM provou ser uma abordagem frutífera para o estudo da mudança de crenças, mas com pouca flexibilidade para investigar fenômenos epistêmicos importantes. Em particular, enquanto as crenças são comumente aceitas como atitudes hiperintensionais, a literatura influenciada por AGM tem se concentrado principalmente em tratamentos intensionais de crenças. Neste trabalho, investigamos operações de mudança de crença hiperintensionais baseadas em uma semântica de mundos impossíveis e mostrando uma forte conexão com operações bem estabelecidas na literatura.
Over the years, the amount of information available to the public by digital means is growing more and more, however, this growth is done in a fragmented way by several companies. Integrating these data may lead to inconsistencies, and system errors. This integration may be difficult and expensive for companies. Data interoperability is done when data with distinct formats or from multiple sources are processed to generate unified data. This work presents a tool to make automatic alignment of data from multiple sources, integrating with the SUMO ontology so that inferences can be made with the tool
We further elaborate, with a short example, on the set of compression rules and the derivation compression algorithm presented in [Haeusler et al. 2023]. We also argue a proof, done with the Lean theorem prover, that this algorithm obtains a dag-like compressed derivation from any tree-like Natural Deduction derivation in Minimal Purely Implicational Logic.
The effort put by an educator on the manual construction of questions may be reduced if one uses tools for the automated generation of questions. Among these tools, only very few are able to control the level of complexity of their output, which ends up representing a challenge for the dissemination of individualized assessments. In the present study, we propose a method for the automated generation of exercises which uses the structure of the solution for the conjecture given as input in order to guarantee the similarity in the level of complexity of these exercises.
