A Reusable Isabelle/HOL Framework for Propositional Labelled Natural Deduction
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Logic/Proof theory
Subject Classification
ACM: Theory of computation~Proof theory
AMS: Mathematical logic and foundations / Proof theory and constructive mathematics
2026
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
2023
2022
Automation of Boolos' Curious Inference in Isabelle/HOL
by Christoph Benzmüller, David Fuenmayor, Alexander Steen and Geoff Sutcliffe
A Sequent Calculus Prover for First-Order Logic with Functions
by Asta Halkjær From and Frederik Krogsdal Jacobsen
2021
2020
An Abstract Formalization of Gödel's Incompleteness Theorems
by Andrei Popescu and Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems—Part II
by Andrei Popescu and Dmitriy Traytel
From Abstract to Concrete Gödel's Incompleteness Theorems—Part I
by Andrei Popescu and Dmitriy Traytel