The Busy Beaver Function
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
David Barros Hulak
E-Mails 📧
Entries
2026
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
A Reusable Isabelle/HOL Framework for Propositional Labelled Natural Deduction
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Mostowski Collapse Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Andrew's Monotone Chain Convex Hull Algorithm
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Alon’s Combinatorial Nullstellensatz
by Arthur Freitas Ramos, Ruy Jose Guerra Barretto de Queiroz and David Barros Hulak
The Classical Seifert–van Kampen Theorem
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Erdos-Ginzburg-Ziv
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Nash Equilibria for Finite Games in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
The Banach–Tarski Paradox in Isabelle/HOL
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Aho-Corasick String Matching
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Nagata Factoriality
by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz