@incollection(sep-brouwer,
author = {Mark van Atten},
year = {2020},
title = {{Luitzen Egbertus Jan Brouwer}},
editor = {Edward N. Zalta},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
edition = {{S}pring 2020},
publisher = {Metaphysics Research Lab, Stanford University},
)
@article(BasinMV98,
author = {David A. Basin and Se{\'{a}}n Matthews and Luca Vigan{\`{o}}},
year = {1998},
title = {Labelled Modal Logics: Quantifiers},
journal = {Journal of Logic, Language and Information},
volume = {7},
number = {3},
pages = {237--263},
doi = {10.1023/A:1008278803780},
)
@inproceedings(Isar08,
author = {Stefan Berghofer and Makarius Wenzel},
year = {2008},
title = {Logic-Free Reasoning in {Isabelle/Isar}},
editor = {Serge Autexier and John A. Campbell and Julio Rubio and Volker Sorge and Masakazu Suzuki and Freek Wiedijk},
booktitle = {Intelligent Computer Mathematics, 9th International Conference, {AISC} 2008, 15th Symposium, Calculemus 2008, 7th International Conference, {MKM} 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5144},
publisher = {Springer},
pages = {355--369},
doi = {10.1007/978-3-540-85110-3\_31},
)
@article(DionisioGM05,
author = {F. Miguel Dion\'{i}sio and Paula Gouveia and Jo{\~{a}}o Marcos},
year = {2005},
title = {Defining and using deductive systems with {Isabelle}},
journal = {Computing, Philosophy, and Cognition},
pages = {271--293},
)
@incollection(dummett1975philosophical,
author = {Michael Dummett},
year = {1975},
title = {The philosophical basis of intuitionistic logic},
booktitle = {Studies in Logic and the Foundations of Mathematics},
volume = {80},
publisher = {Elsevier},
pages = {5--40},
)
@book(dummett2000elements,
author = {Michael Dummett},
year = {2000},
title = {Elements of intuitionism},
publisher = {Oxford University Press},
)
@inproceedings(ThEdu19,
author = {Asta Halkj{\ae}r From and Alexander Birch Jensen and Anders Schlichtkrull and J{\o}rgen Villadsen},
year = {2019},
title = {Teaching a Formalized Logical Calculus},
editor = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
booktitle = {Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019},
series = {{EPTCS}},
volume = {313},
pages = {73--92},
doi = {10.4204/EPTCS.313.5},
)
@inproceedings(ThEdu20,
author = {Asta Halkj{\ae}r From and J{\o}rgen Villadsen and Patrick Blackburn},
year = {2020},
title = {Isabelle/{HOL} as a Meta-Language for Teaching Logic},
editor = {Pedro Quaresma and Walther Neuper and Jo{\~{a}}o Marcos},
booktitle = {Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, Paris, France, 29th June 2020},
series = {{EPTCS}},
volume = {328},
pages = {18--34},
doi = {10.4204/EPTCS.328.2},
)
@article(FOL-Axiomatic-AFP,
author = {Asta Halkj\IeC{\ae}r From},
year = {2021},
title = {Soundness and Completeness of an Axiomatic System for First-Order Logic},
journal = {Archive of Formal Proofs},
note = {\url{https://isa-afp.org/entries/FOL_Axiomatic.html}, Formal proof development},
)
@incollection(sep-intuitionism,
author = {Rosalie Iemhoff},
year = {2020},
title = {{Intuitionism in the Philosophy of Mathematics}},
editor = {Edward N. Zalta},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
edition = {{F}all 2020},
publisher = {Metaphysics Research Lab, Stanford University},
)
@incollection(sep-logic-intuitionistic,
author = {Joan Moschovakis},
year = {2021},
title = {{Intuitionistic Logic}},
editor = {Edward N. Zalta},
booktitle = {The {Stanford} Encyclopedia of Philosophy},
edition = {{F}all 2021},
publisher = {Metaphysics Research Lab, Stanford University},
)
@book(nipkow+02,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
year = {2002},
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
series = {Lecture Notes in Computer Science},
volume = {2283},
publisher = {Springer},
doi = {10.1007/3-540-45949-9},
)
@article(Paulson89,
author = {Lawrence C. Paulson},
year = {1989},
title = {The Foundation of a Generic Theorem Prover},
journal = {J. Autom. Reason.},
volume = {5},
number = {3},
pages = {363--397},
doi = {10.1007/BF00248324},
)
@inproceedings(ThEdu18,
author = {Anders Schlichtkrull and J{\o}rgen Villadsen and Andreas Halkj{\ae}r From},
year = {2018},
title = {Students' Proof Assistant {(SPA)}},
editor = {Pedro Quaresma and Walther Neuper},
booktitle = {Proceedings 7th International Workshop on Theorem proving components for Educational software, THedu@FLoC 2018, Oxford, United Kingdom, 18 july 2018},
series = {{EPTCS}},
volume = {290},
pages = {1--13},
doi = {10.4204/EPTCS.290.1},
)
@inproceedings(ThEdu17,
author = {J{\o}rgen Villadsen and Andreas Halkj{\ae}r From and Anders Schlichtkrull},
year = {2017},
title = {Natural Deduction and the {Isabelle} Proof Assistant},
editor = {Pedro Quaresma and Walther Neuper},
booktitle = {Proceedings 6th International Workshop on Theorem proving components for Educational software, ThEdu@CADE 2017, Gothenburg, Sweden, 6 Aug 2017},
series = {{EPTCS}},
volume = {267},
pages = {140--155},
doi = {10.4204/EPTCS.267.9},
)
@inproceedings(PAAR,
author = {J{\o}rgen Villadsen and Anders Schlichtkrull and Andreas Halkj{\ae}r From},
year = {2018},
title = {A Verified Simple Prover for First-Order Logic},
editor = {Boris Konev and Josef Urban and Philipp R{\"{u}}mmer},
booktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR 2018) co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, 19 July 2018},
series = {{CEUR} Workshop Proceedings},
volume = {2162},
publisher = {CEUR-WS.org},
pages = {88--104},
url = {http://ceur-ws.org/Vol-2162/paper-08.pdf},
)
@inproceedings(Pure08,
author = {Makarius Wenzel and Lawrence C. Paulson and Tobias Nipkow},
year = {2008},
title = {The {Isabelle} Framework},
editor = {Otmane A{\"{\i}}t Mohamed and Mu{\~{n}}oz, C{\'{e}}sar A. and Sofi{\`{e}}ne Tahar},
booktitle = {Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5170},
publisher = {Springer},
pages = {33--38},
doi = {10.1007/978-3-540-71067-7\_7},
)