Ausgabe 1/2023
Inhalt (13 Artikel)
Formalising Szemerédi’s Regularity Lemma and Roth’s Theorem on Arithmetic Progressions in Isabelle/HOL
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
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
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ć
Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
Dominik Kirst, Marc Hermes