Amb motiu del tancament d'estiu, la validació de documents es reprendrà a partir del 28 d'agost de 2026. Disculpeu les molèsties.
Con motivo del cierre de verano, la validación de documentos se reanudará a partir del 28 de agosto de 2026. Disculpad las molestias
Due to the summer closure, document validation will resume starting August 28, 2026. We apologize for any inconvenience.

Files

When_the_laws_of_logic_meet_the_logic_of_laws.pdf (981.78 KB)

Document type

Master thesis

Publication date

2018

Publication license

cc-by-nc-nd (c) Castillo Tierz, 2018
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/133778

When the laws of logic meet the logic of laws

Journal Title

Authors

Director/Tutor

Journal ISSN

Volume Title

Related resource

Abstract

This master thesis presents a brief introduction to type theory, starting at the simplest systems and building up to the Calculus of Inductive Constructions, the formal theory that lies behind some software tools called 'proof assistants'. We will then study a real-life problem based on an actual law (European Regulation 561 for Road Transport) and show that there exist ambiguous situations. Finally, we will use Coq, a proof assistant, to draft the correctness checking proof of our results on the law.

Description

Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten

Subject

Lògica, Teoria de tipus, Treballs de fi de màster

Subject (English)

Logic, Type theory, Master's theses

Citation

Collections

Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

Citation

DEL CASTILLO TIERZ, Jorge del. When the laws of logic meet the logic of laws. [consulted: 13 of August of 2026]. Available at: https://hdl.handle.net/2445/133778

Export metadata

JSON - METS

Share record