Angeliki Koutsoukou-Argyraki
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Previous Organizations / Institutes
The organizations / institutes from the scholar's other articles in the past ten years
Angeliki Koutsoukou-Argyraki has a total of 6 co-authors. Here are the top co-authors by number of shared publications:
- Lawrence Charles Paulson
University of Cambridge
6 shared publications - Chelsea Edmonds
Department of Computer Science and Technology University of Cambridge UK
2 shared publications - Wenda Li
Computer Laboratory Computer Laboratory University of Cambridge University of Cambridge
2 shared publications - Karol Wapniarski
University of Cambridge
1 shared publication - Mirna Džamonja
School of Mathematics University of East Anglia Norwich NR4 7TJ UK
1 shared publication - Mirna Džamonja
IRIF(CNRS & Université de Paris-Cité)
1 shared publication
Latest Publications
- Open Access
- 18 April 2025
- Published by Springer Nature in Topoi
- Vol. 45 (2) , 693-705
A Formalisation of Aristotle’s Assertoric Syllogistic in Isabelle/HOL
We present a formalisation of Aristotle’s Assertoric Syllogistic in the proof assistant (interactive theorem prover) Isabelle/HOL and discuss the insights gained by the formalisation, as we demonstrate that the formal proofs and especially Isabelle’s automation can enhance the user’s understanding and facilitate metatheoretical explorations.
- 18 April 2025
- Published by Springer Nature in Topoi
- Vol. 45 (2) , 693-705
Open AccessA Formalisation of Aristotle’s Assertoric Syllogistic in Isabelle/HOL
We present a formalisation of Aristotle’s Assertoric Syllogistic in the proof assistant (interactive theorem prover) Isabelle/HOL and discuss the insights gained by the formalisation, as we demonstrate that the formal proofs and especially Isabelle’s automation can enhance the user’s understanding and facilitate metatheoretical explorations.
- Open Access
- 19 December 2022
- Published by Springer Nature in Journal of Automated Reasoning
- Vol. 67 (1) , 1-21
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
- 19 December 2022
- Published by Springer Nature in Journal of Automated Reasoning
- Vol. 67 (1) , 1-21
Open AccessFormalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
- Open Access
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
Open AccessFormalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
We have formalised Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the former to first show the Triangle Counting Lemma and the Triangle Removal Lemma: themselves important technical results. Here, in addition to showcasing the main formalised statements and definitions, we focus on sensitive points in the proofs, describing how we overcame the difficulties that we encountered.
- Open Access
- 21 October 2021
- Published by Taylor & Francis in Experimental Mathematics
- Vol. 31 (2) , 401-412
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erdős and Straus, Hančl, and Hančl and Rucki. Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.
- 21 October 2021
- Published by Taylor & Francis in Experimental Mathematics
- Vol. 31 (2) , 401-412
Open AccessIrrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erdős and Straus, Hančl, and Hančl and Rucki. Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.
- Open Access
- 11 October 2021
- Published by Taylor & Francis in Experimental Mathematics
- Vol. 31 (2) , 383-400
Formalizing Ordinal Partition Relations Using Isabelle/HOL
This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all , . This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.- 11 October 2021
- Published by Taylor & Francis in Experimental Mathematics
- Vol. 31 (2) , 383-400
Open AccessFormalizing Ordinal Partition Relations Using Isabelle/HOL
This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all , . This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic. - 2 July 2021
- Published by Springer Nature
- p. 285-296
On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy
- 2 July 2021
- Published by Springer Nature
- p. 285-296
On Preserving the Computational Content of Mathematical Proofs: Toy Examples for a Formalising Strategy
- Open Access
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erd\H{o}s and Straus (1974), Han\v{c}l (2002), and Han\v{c}l and Rucki (2005). Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.
Open AccessIrrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL
We give an overview of our formalizations in the proof assistant Isabelle/HOL of certain irrationality and transcendence criteria for infinite series from three different research papers: by Erd\H{o}s and Straus (1974), Han\v{c}l (2002), and Han\v{c}l and Rucki (2005). Our formalizations in Isabelle/HOL can be found on the Archive of Formal Proofs. Here we describe selected aspects of the formalization and discuss what this reveals about the use and potential of Isabelle/HOL in formalizing modern mathematical research, particularly in these parts of number theory and analysis.
- Open Access
Formalising Ordinal Partition Relations Using Isabelle/HOL
This is an overview of a formalisation project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erd\H{o}s--Milner, Specker, Larson and Nash-Williams, leading to Larson's proof of the unpublished result by E.C. Milner asserting that for all $m \in \mathbb{N}$, $\omega^\omega\arrows(\omega^\omega, m)$. This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalisation process. This project is also a demonstration of working with Zermelo-Fraenkel set theory in higher-order logic.Open AccessFormalising Ordinal Partition Relations Using Isabelle/HOL
This is an overview of a formalisation project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erd\H{o}s--Milner, Specker, Larson and Nash-Williams, leading to Larson's proof of the unpublished result by E.C. Milner asserting that for all $m \in \mathbb{N}$, $\omega^\omega\arrows(\omega^\omega, m)$. This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalisation process. This project is also a demonstration of working with Zermelo-Fraenkel set theory in higher-order logic. - Open Access
- 6 October 2020
- Published by Springer Fachmedien Wiesbaden GmbH in Jahresbericht der Deutschen Mathematiker-Vereinigung
- Vol. 123 (1) , 3-26
Formalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started
This is an account of a mathematician’s first experiences with the proof assistant (interactive theorem prover) Isabelle/HOL, including a discussion on the rationale behind formalising mathematics and the choice of Isabelle/HOL in particular, some instructions for new users, some technical and conceptual observations focussing on some of the first difficulties encountered, and some thoughts on the use and potential of proof assistants for mathematics.
- 6 October 2020
- Published by Springer Fachmedien Wiesbaden GmbH in Jahresbericht der Deutschen Mathematiker-Vereinigung
- Vol. 123 (1) , 3-26
Open AccessFormalising Mathematics – in Praxis; A Mathematician’s First Experiences with Isabelle/HOL and the Why and How of Getting Started
This is an account of a mathematician’s first experiences with the proof assistant (interactive theorem prover) Isabelle/HOL, including a discussion on the rationale behind formalising mathematics and the choice of Isabelle/HOL in particular, some instructions for new users, some technical and conceptual observations focussing on some of the first difficulties encountered, and some thoughts on the use and potential of proof assistants for mathematics.
- Open Access
- 1 January 2018
- Published by Journal of Logic and Analysis in Journal of Logic and Analysis
- Vol. 10, 1-30
New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups
New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups
- 1 January 2018
- Published by Journal of Logic and Analysis in Journal of Logic and Analysis
- Vol. 10, 1-30
Open AccessNew effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups
New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups