Modal Logic Library in Coq

Tabela de conteúdos

<!--ts-->

• Abstract
• Technology
• Compile
• License
• Reference
• Authors

<!--te-->

Abstract

The modelling of certain types of computational systems with classical logic includes limiting factors. In this context, the presentation of other logical systems, such as modal logic, and the construction of a library for the proof assistant Coq intents to help in the modelling and facilitate usage on the verification of systems' properties. The semantics of modal logic is represented by the semantics of possible worlds, where there is an accessibility relationship that connects the worlds of a model. Different restrictions imposed on the accessibility relation build modal logic systems that help representation of properties on a wide array of research areas. The libary development aims to held the formalization of properties in softwares and prove them on Coq.

Technology

• Coq

Compile

In the project directory, you can run:

$ make

License

BSD-2-Clause

Reference

SILVEIRA, Ariel Agne da; ROGGIA, Karina Girardi; TORRENS, Paulo Henrique. Implementação de uma biblioteca de lógica modal em Coq. 2020. 65 f. Trabalhos de Conclusão de Curso (Graduação)-Universidade do Estado de Santa Catarina, Centro de Ciências Tecnológicas, Curso de Curso de Ciência da Computação, Joinville, 2020.

Authors

---

Search Group: FUNÇÃO

<table> <tr> <td> <img style="border-radius: 50%;" src="https://avatars1.githubusercontent.com/u/19842910?v=4" width="100px;" alt=""> <br/> _{Author: <a href="https://github.com/arielsilveira"><b>Ariel Agne da Silveira</b>} </a> </td> <td> <img style="border-radius: 50%;" src="https://avatars2.githubusercontent.com/u/6727632?v=4" width="100px;" alt=""> <br/> _{Advisor: <a href="https://github.com/kaqui"><b>Karina Girardi Roggia</b>} </a> </td> <td> <img style="border-radius: 50%;" src="https://avatars3.githubusercontent.com/u/394865?v=4" width="100px;" alt=""> <br/> _{Co-Advisor: <a href="https://github.com/takanuva"><b>Paulo Henrique Torrens</b>} </a> </td> </tr> </table> <!-- [](mailto:ariel.agne95@gmail.com) -->