Agent-Based Logics in Dependent Type Theory
This thesis is on the formalisation of mathematics in Martin-Löf type theory. This is a class of dependently-typed functional programming languages whose rules form a language suitable for the statement and proof of mathematical theorems. Programs in type theory can be mechanically checked to be wel...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/81134/ |
| _version_ | 1848801295857614848 |
|---|---|
| author | Baston, Colm |
| author_facet | Baston, Colm |
| author_sort | Baston, Colm |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | This thesis is on the formalisation of mathematics in Martin-Löf type theory. This is a class of dependently-typed functional programming languages whose rules form a language suitable for the statement and proof of mathematical theorems. Programs in type theory can be mechanically checked to be well-typed, which corresponds to proofs being checked to be valid. In particular, we explore the semantics of certain agent-based logics, and seek to give them appropriate representations using the concepts of type theory.
We embed the syntax of epistemic modal logic in type theory as predicates over a type of possible worlds. Knowledge operators are defined in this setting by stating a set of properties they must satisfy. We prove this knowledge operator semantics equivalent to the traditional relational semantics of epistemic logic. Common knowledge is then defined in the embedding as a coinductive predicate, whose proofs are infinite data structures. We prove this representation is equivalent to the intuitive definition as iterated universal knowledge, and prove it is equivalent to the relational interpretation. In coalition logic, we represent game forms and playable effectivity functions in type theory, and outline a proof of their equivalence. |
| first_indexed | 2025-11-14T21:05:11Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-81134 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T21:05:11Z |
| publishDate | 2025 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-811342025-08-11T14:17:01Z https://eprints.nottingham.ac.uk/81134/ Agent-Based Logics in Dependent Type Theory Baston, Colm This thesis is on the formalisation of mathematics in Martin-Löf type theory. This is a class of dependently-typed functional programming languages whose rules form a language suitable for the statement and proof of mathematical theorems. Programs in type theory can be mechanically checked to be well-typed, which corresponds to proofs being checked to be valid. In particular, we explore the semantics of certain agent-based logics, and seek to give them appropriate representations using the concepts of type theory. We embed the syntax of epistemic modal logic in type theory as predicates over a type of possible worlds. Knowledge operators are defined in this setting by stating a set of properties they must satisfy. We prove this knowledge operator semantics equivalent to the traditional relational semantics of epistemic logic. Common knowledge is then defined in the embedding as a coinductive predicate, whose proofs are infinite data structures. We prove this representation is equivalent to the intuitive definition as iterated universal knowledge, and prove it is equivalent to the relational interpretation. In coalition logic, we represent game forms and playable effectivity functions in type theory, and outline a proof of their equivalence. 2025-07-30 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en cc_by https://eprints.nottingham.ac.uk/81134/1/thesis.pdf Baston, Colm (2025) Agent-Based Logics in Dependent Type Theory. PhD thesis, University of Nottingham. functional programming languages Martin-Löf type theory modal logic |
| spellingShingle | functional programming languages Martin-Löf type theory modal logic Baston, Colm Agent-Based Logics in Dependent Type Theory |
| title | Agent-Based Logics in Dependent Type Theory |
| title_full | Agent-Based Logics in Dependent Type Theory |
| title_fullStr | Agent-Based Logics in Dependent Type Theory |
| title_full_unstemmed | Agent-Based Logics in Dependent Type Theory |
| title_short | Agent-Based Logics in Dependent Type Theory |
| title_sort | agent-based logics in dependent type theory |
| topic | functional programming languages Martin-Löf type theory modal logic |
| url | https://eprints.nottingham.ac.uk/81134/ |