A Formalisation of Aristotle’s Assertoric Syllogistic in Isabelle/HOL
Abstract 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.
Authors
- Angeliki Koutsoukou-Argyraki (ORCID: https://orcid.org/0000-0002-8886-5281)
- Karol Wapniarski (ORCID: https://orcid.org/0009-0001-4877-9370)
Institutions
- Royal Holloway University of London (GB)
- University of Cambridge (GB)
- Adam Mickiewicz University in Poznań (PL)
Publication Details
- Journal
- Topoi
- Published
- 2025-04-18
- DOI
- https://doi.org/10.1007/s11245-025-10184-6
- Primary Topic
- Classical Antiquity Studies
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Eberhard Karls Universität Tübingen
- Aristotle University of Thessaloniki
- European Research Council