Please use this identifier to cite or link to this item:
http://hdl.handle.net/2445/133778| Title: | When the laws of logic meet the logic of laws |
| Author: | del Castillo Tierz, Jorge del |
| Keywords: | Lògica Teoria de tipus Treballs de fi de màster Logic Type theory Master's theses |
| Issue Date: | 2018 |
| 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. |
| Note: | Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona, Curs: 2017-2018, Tutor: Joost J. Joosten |
| URI: | http://hdl.handle.net/2445/133778 |
| Appears in Collections: | Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| When_the_laws_of_logic_meet_the_logic_of_laws.pdf | 981.78 kB | Adobe PDF | View/Open |
This item is licensed under a
Creative Commons License
