Search Results

Documents authored by Schlichtkrull, Anders

Artifact
Software
DOI: 10.4230/artifacts.23798
Analytic Completeness

Authors: Asta Halkjær From and Anders Schlichtkrull

Abstract
Cite as

Asta Halkjær From, Anders Schlichtkrull. Analytic Completeness (Software, Mechanization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23798,
   title = {{Analytic Completeness}}, 
   author = {From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f;origin=https://github.com/astahfrom/Analytic_Completeness;visit=swh:1:snp:1c9ea048be7f3b4c9f6ed573e2d87ba0b8480717;anchor=swh:1:rev:cd6a06dd8478287763c6e820e51581322faa7f2c}{\texttt{swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f}} (visited on 2025-09-22)},
   url = {https://github.com/astahfrom/Analytic_Completeness},
   doi = {10.4230/artifacts.23798},
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.8
Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting

Authors: Asta Halkjær From and Anders Schlichtkrull

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Smullyan and Fitting have used abstract consistency properties to great effect in unifying meta-theoretical results in logic. In this paper, we generalize these developments with the help of Isabelle/HOL. We use locales to decompose abstract consistency into general parts, and provide the textbook variants as special cases. Users can assemble their own consistency property for a given logic. The compositionality alleviates the absence of dependent types in Isabelle/HOL. We use our development to mechanize completeness of calculi for three logics: (1) first-order logic where we only instantiate universal quantifiers with already occurring terms, (2) second-order logic over general models, and (3) a recently developed strong hybrid logic with propositional quantification.
Cite as

Asta Halkjær From and Anders Schlichtkrull. Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness à la Fitting. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{from_et_al:LIPIcs.ITP.2025.8,
  author =	{From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
  title =	{{Abstract, Compositional Consistency: Isabelle/HOL Locales for Completeness \`{a} la Fitting}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.8},
  URN =		{urn:nbn:de:0030-drops-246406},
  doi =		{10.4230/LIPIcs.ITP.2025.8},
  annote =	{Keywords: Logic, completeness, abstract consistency property, Isabelle/HOL, locales}
}
Document
DOI: 10.4230/OASIcs.ICPEC.2023.14
An Experience with and Reflections on Live Coding with Active Learning

Authors: Anders Schlichtkrull

Published in: OASIcs, Volume 112, 4th International Computer Programming Education Conference (ICPEC 2023)

Abstract
In this paper I report and reflect on a concrete experience with changing an introductory programming course from being based on "classical lectures" to being based on live coding with active learning. The experiment is built on learnings found in the literature and the pedagogical theories of scaffolding, think-pair-share and teaching as facilitation of learning. I reflect on the students' reaction to the experiment, the difficulty of the active learning, how to keep time, coverage of learning objectives, the degree of improvisation and student involvement. The experiment was well received by the students, and I report also on the feedback. My hope is that educators who want to introduce live coding with active learning will be able to draw inspiration from my preparation of, execution of and reflections on the experiment.
Cite as

Anders Schlichtkrull. An Experience with and Reflections on Live Coding with Active Learning. In 4th International Computer Programming Education Conference (ICPEC 2023). Open Access Series in Informatics (OASIcs), Volume 112, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{schlichtkrull:OASIcs.ICPEC.2023.14,
  author =	{Schlichtkrull, Anders},
  title =	{{An Experience with and Reflections on Live Coding with Active Learning}},
  booktitle =	{4th International Computer Programming Education Conference (ICPEC 2023)},
  pages =	{14:1--14:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-290-7},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{112},
  editor =	{Peixoto de Queir\'{o}s, Ricardo Alexandre and Teixeira Pinto, M\'{a}rio Paulo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2023.14},
  URN =		{urn:nbn:de:0030-drops-185108},
  doi =		{10.4230/OASIcs.ICPEC.2023.14},
  annote =	{Keywords: Live coding, active learning, teaching programming}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2018.5
New Formalized Results on the Meta-Theory of a Paraconsistent Logic

Authors: Anders Schlichtkrull

Published in: LIPIcs, Volume 130, 24th International Conference on Types for Proofs and Programs (TYPES 2018)

Abstract
Classical logics are explosive, meaning that everything follows from a contradiction. Paraconsistent logics are logics that are not explosive. This paper presents the meta-theory of a paraconsistent infinite-valued logic, in particular new results showing that while the question of validity for a given formula can be reduced to a consideration of only finitely many truth values, this does not mean that the logic collapses to a finite-valued logic. All definitions and theorems are formalized in the Isabelle/HOL proof assistant.
Cite as

Anders Schlichtkrull. New Formalized Results on the Meta-Theory of a Paraconsistent Logic. In 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{schlichtkrull:LIPIcs.TYPES.2018.5,
  author =	{Schlichtkrull, Anders},
  title =	{{New Formalized Results on the Meta-Theory of a Paraconsistent Logic}},
  booktitle =	{24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  pages =	{5:1--5:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-106-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{130},
  editor =	{Dybjer, Peter and Esp{\'\i}rito Santo, Jos\'{e} and Pinto, Lu{\'\i}s},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2018.5},
  URN =		{urn:nbn:de:0030-drops-114098},
  doi =		{10.4230/LIPIcs.TYPES.2018.5},
  annote =	{Keywords: Paraconsistent logic, Many-valued logic, Formalization, Isabelle proof assistant, Paraconsistency}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact