3 citations · 3 across the 7 of their papers we have counts for
8 papers
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
We present a Lean 4 Mathlib formalization of Nagata's factoriality theorem: if R is a noetherian domain and S <= R is a prime-generated submonoid such that S^{-1}R is a UFD, then R…
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of c…
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz +1
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting…
Computational Paths Form a Weak ω-Groupoid
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-Löf type theory carry the structure of weak ω-groupoids. Their proofs, while foundational, rely on abstr…
Formalizing Computational Paths and Fundamental Groups in Lean
Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz +1
Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborato…
Meaning as Use, Application, Employment, Purpose, Usefulness
Ruy J. G. B. de Queiroz
Arising from the whole body of Wittgenstein's writings is a picture of a (not necessarily straight, linear, but admittedly tireless) journey to come to terms with the mechanics of…
From the Notebooks to the Investigations and Beyond
Ruy J. G. B. de Queiroz
The use of the open and searchable Wittgenstein's Nachlass (The Wittgenstein Archives at the University of Bergen (WAB)) has proved instrumental in the quest for a common thread of…
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define…