A framework for relating, implementing and verifying argumentation models and their translations
Computational argumentation theory deals with the formalisation of argument structure, conflict between arguments and domain-specific constructs, such as proof standards, epistemic probabilities or argument schemes. However, despite these practical components, there is a lack of implementations and...
| Main Author: | |
|---|---|
| Format: | Thesis (University of Nottingham only) |
| Language: | English |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/32798/ |
| _version_ | 1848794492191113216 |
|---|---|
| author | van Gijzel, Bas |
| author_facet | van Gijzel, Bas |
| author_sort | van Gijzel, Bas |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Computational argumentation theory deals with the formalisation of argument structure, conflict between arguments and domain-specific constructs, such as proof standards, epistemic probabilities or argument schemes. However, despite these practical components, there is a lack of implementations and implementation methods available for most structured models of argumentation and translations between them.
This thesis addresses this problem, by constructing a general framework for relating, implementing and formally verifying argumentation models and translations between them, drawing from dependent type theory and the Curry-Howard correspondence. The framework provides mathematical tools and programming methodologies to implement argumentation models, allowing programmers and argumentation theorists to construct implementations that are closely related to the mathematical definitions. It furthermore provides tools that, without much effort on the programmer's side, can automatically construct counter-examples to desired properties, while finally providing methodologies that can prove formal correctness of the implementation in a theorem prover.
The thesis consists of various use cases that demonstrate the general approach of the framework. The Carneades argumentation model, Dung's abstract argumentation frameworks and a translation between them, are implemented in the functional programming language Haskell. Implementations of formal properties of the translation are provided together with a formalisation of AFs in the theorem prover, Agda. The result is a verified pipeline, from the structured model Carneades into existing efficient SAT-based implementations of Dung's AFs. Finally, the ASPIC+ model for argumentation is generalised to incorporate content orderings, weight propagation and argument accrual. The framework is applied to provide a translation from this new model into Dung's AFs, together with a complete implementation. |
| first_indexed | 2025-11-14T19:17:03Z |
| format | Thesis (University of Nottingham only) |
| id | nottingham-32798 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-14T19:17:03Z |
| publishDate | 2016 |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-327982017-10-13T17:31:58Z https://eprints.nottingham.ac.uk/32798/ A framework for relating, implementing and verifying argumentation models and their translations van Gijzel, Bas Computational argumentation theory deals with the formalisation of argument structure, conflict between arguments and domain-specific constructs, such as proof standards, epistemic probabilities or argument schemes. However, despite these practical components, there is a lack of implementations and implementation methods available for most structured models of argumentation and translations between them. This thesis addresses this problem, by constructing a general framework for relating, implementing and formally verifying argumentation models and translations between them, drawing from dependent type theory and the Curry-Howard correspondence. The framework provides mathematical tools and programming methodologies to implement argumentation models, allowing programmers and argumentation theorists to construct implementations that are closely related to the mathematical definitions. It furthermore provides tools that, without much effort on the programmer's side, can automatically construct counter-examples to desired properties, while finally providing methodologies that can prove formal correctness of the implementation in a theorem prover. The thesis consists of various use cases that demonstrate the general approach of the framework. The Carneades argumentation model, Dung's abstract argumentation frameworks and a translation between them, are implemented in the functional programming language Haskell. Implementations of formal properties of the translation are provided together with a formalisation of AFs in the theorem prover, Agda. The result is a verified pipeline, from the structured model Carneades into existing efficient SAT-based implementations of Dung's AFs. Finally, the ASPIC+ model for argumentation is generalised to incorporate content orderings, weight propagation and argument accrual. The framework is applied to provide a translation from this new model into Dung's AFs, together with a complete implementation. 2016-07-15 Thesis (University of Nottingham only) NonPeerReviewed application/pdf en cc_by https://eprints.nottingham.ac.uk/32798/1/thesis.pdf van Gijzel, Bas (2016) A framework for relating, implementing and verifying argumentation models and their translations. PhD thesis, University of Nottingham. argumentation theory functional programming Haskell Agda Carneades domain specific language theorem proving dependent type theory argumentation model implementation |
| spellingShingle | argumentation theory functional programming Haskell Agda Carneades domain specific language theorem proving dependent type theory argumentation model implementation van Gijzel, Bas A framework for relating, implementing and verifying argumentation models and their translations |
| title | A framework for relating, implementing and verifying argumentation models and their translations |
| title_full | A framework for relating, implementing and verifying argumentation models and their translations |
| title_fullStr | A framework for relating, implementing and verifying argumentation models and their translations |
| title_full_unstemmed | A framework for relating, implementing and verifying argumentation models and their translations |
| title_short | A framework for relating, implementing and verifying argumentation models and their translations |
| title_sort | framework for relating, implementing and verifying argumentation models and their translations |
| topic | argumentation theory functional programming Haskell Agda Carneades domain specific language theorem proving dependent type theory argumentation model implementation |
| url | https://eprints.nottingham.ac.uk/32798/ |