A. A. Borges, M. González Bedmar, J. J. Conejero Rodríguez, E. Hermo Reyes, J. Casals Buñuel, and J. J. Joosten
FV Time: a formally verified Coq library
arXiv:2209.14227 [cs.SE]
2022
Coq code
A. A. Borges
Towards a Coq formalization of a quantified modal logic
Proceedings of the 4th Workshop on Automated Reasoning in Quantified Non-Classical Logics: 13-27
2022
Coq code
A. A. Borges, and J. J. Joosten
An Escape from Vardanyan’s Theorem
Journal of Symbolic Logic
arXiv:2102.13091 [math.LO]
2022
A. A. Borges, J. J. Conejero Rodríguez, D. Fernández-Duque, M. González. Bedmar, and J. J. Joosten
To drive or not to drive: A logical and computational analysis of European transport regulations
Information and Computation 280
2021
A. A. Borges, and J. J. Joosten
Quantified Reflection Calculus with one modality
Advances in Modal Logic 13: 13-32
2020
A. A. Borges, J. J. Conejero Rodríguez, D. Fernández-Duque, M. González Bedmar, and J. J. Joosten
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations
26th International Symposium on Temporal Representation and Reasoning (TIME 2019): 6:1-6:16
2019
A. A. Borges, and J. J. Joosten
The Worm Calculus
Advances in Modal Logic 12: 13-27
2018
This paper was partly formalized in Coq.
A. A. Borges
On the herbrandised interpretation for nonstandard arithmetic
Master’s Thesis, Universidade de Lisboa
2016