Issue 1/2023
Content (13 Articles)
Open Access
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Open Access
Measuring the Readability of Geometric Proofs: The Area Method Case
Pedro Quaresma, Pierluigi Graziani
Semantically-Guided Goal-Sensitive Reasoning: Decision Procedures and the Koala Prover
Maria Paola Bonacina, Sarah Winkler
Optimal Deterministic Controller Synthesis from Steady-State Distributions
Alvaro Velasquez, Ismail Alkhouri, K. Subramani, Piotr Wojciechowski, George Atia
Open Access
Correction
Correction: Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL
Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot
Superposition for Higher-Order Logic
Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, Petar Vukmirović
Open Access
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
Dominik Kirst, Marc Hermes