Cover Image

Ruitenburg's Theorem Mechanized and Contextualized

Fuente: arXiv

Saved in:

Bibliographic Details
Main Author:	Litak, Tadeusz
Format:	Preprint
Published:	2024
Subjects:	Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Relational semantics for flat Heyting-Lewis Logic
by: de Groot, Jim, et al.
Published: (2026)

Bounded Inquisitive Logics: Sequent Calculi and Schematic Validity
by: Litak, Tadeusz, et al.
Published: (2025)

Gödel-McKinsey-Tarski and (not quite) Blok-Esakia for Heyting-Lewis Implication
by: de Groot, Jim, et al.
Published: (2021)

Lewis and Brouwer meet Strong Löb
by: Visser, Albert, et al.
Published: (2024)

Inquisitive Team Semantics of LTL
by: Bozzelli, Laura, et al.
Published: (2025)

Comparing and Contrasting Arrow's Impossibility Theorem and Gödel's Incompleteness Theorem
by: Livson, Ori, et al.
Published: (2025)

Fixed Point Theorems in Computability Theory
by: Terwijn, Sebastiaan A.
Published: (2024)

An Analysis of Tennenbaum's Theorem in Constructive Type Theory
by: Hermes, Marc, et al.
Published: (2023)

Gödel Incompleteness Theorem for PAC Learnable Theory from the view of complexity measurement
by: Ma, Zhifeng, et al.
Published: (2024)

Functional variant of Polynomial Analogue of Gandy's Fixed Point Theorem
by: Nechesov, Andrey
Published: (2024)

Advances in Algorithmic Meta Theorems
by: Siebertz, Sebastian, et al.
Published: (2024)

Lovász Theorems for Modal Languages
by: Comer, Jesse
Published: (2024)

Algorithmic Perspective on Toda's Theorem
by: Fried, Dror, et al.
Published: (2025)

Preservation Theorems in Semiring Semantics
by: Brinke, Sophie, et al.
Published: (2026)

Locality Theorems in Semiring Semantics
by: Bizière, Clotilde, et al.
Published: (2023)

On Effective Banach-Mazur Games and an application to the Poincaré Recurrence Theorem for Category
by: Koul, Prajval, et al.
Published: (2025)

An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction
by: Xu, Yang, et al.
Published: (2025)

Codd's Theorem for Databases over Semirings
by: Badia, Guillermo, et al.
Published: (2025)

Generating Theorems by Generating Proof Structures
by: Wernhard, Christoph
Published: (2026)

A Dichotomy Theorem for Ordinal Ranks in MSO
by: Niwiński, Damian, et al.
Published: (2025)

Equational Theorem Proving for Clauses over Strings
by: Kim, Dohan
Published: (2023)

A No-go Theorem for Coalgebraic Product Construction
by: Kori, Mayuko, et al.
Published: (2025)

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq
by: Affeldt, Reynald, et al.
Published: (2024)

Formalizing Representation Theorems for a Logical Framework with Rewriting
by: Traversié, Thomas, et al.
Published: (2025)

Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
by: Meseguer, Jose
Published: (2024)

A General Completeness Theorem for Skip-free Star Algebras
by: Kappé, Tobias, et al.
Published: (2025)

HHLPar: Automated Theorem Prover for Parallel Hybrid Communicating Sequential Processes
by: Jin, Xiangyu, et al.
Published: (2024)

LLM-Powered Automatic Theorem Proving and Synthesis for Hybrid Systems and Game
by: Kabra, Aditi, et al.
Published: (2026)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

Yeo's Theorem for Locally Colored Graphs: the Path to Sequentialization in Linear Logic
by: Di Guardia, Rémi, et al.
Published: (2026)

Fagin's Theorem for Semiring Turing Machines
by: Badia, Guillermo, et al.
Published: (2025)

Preservation Theorems for Unravelling-Invariant Classes: A Uniform Approach for Modal Logics and Graph Neural Networks
by: Wałęga, Przemysław Andrzej, et al.
Published: (2026)

Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
by: Kirst, Dominik, et al.
Published: (2026)

Linear Contextual Metaprogramming and Session Types
by: Ângelo, Pedro, et al.
Published: (2024)

Commutation Groups and State-Independent Contextuality
by: Abramsky, Samson, et al.
Published: (2026)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
by: Ji, Junye
Published: (2026)

Composition Direction of Seymour's Theorem for Regular Matroids -- Formally Verified
by: Dvorak, Martin, et al.
Published: (2025)

Automated Theorem Proving for Prolog Verification
by: Mesnard, Fred, et al.
Published: (2026)

Partial Label Learning for Automated Theorem Proving
by: Zombori, Zsolt, et al.
Published: (2025)

Vibe Coding an LLM-powered Theorem Prover
by: Hou, Zhe
Published: (2026)