output
20072026
most citedDeriving reproducible biomarkers from multi-site resting-state data: An Autism-based example

742 citations

researchers with a paper here
collaborating institutions
Showing 2023 · cs.LOShow all

23 papers · 2 filters

cs.LO2023

Peano Arithmetic and MALL

Matteo Manighetti, Dale Miller

Formal theories of arithmetic have traditionally been based on either classical or intuitionistic logic, leading to the development of Peano and Heyting arithmetic, respectively. W…

cs.LO2023★ 6 cited

Dedukti: a Logical Framework based on the -Calculus Modulo Theory

Ali Assaf, Guillaume Burel, Raphaël Cauderlier +7

Dedukti is a Logical Framework based on the -Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simpl…

cs.LO2023★ 1 cited

Cut elimination for Zermelo set theory

Gilles Dowek, Alexandre Miquel

We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof en…

cs.LO2023★ 2 cited

Relative normalization

Gilles Dowek, Alexandre Miquel

G{ö}del's second incompleteness theorem forbids to prove, in a given theory U, the consistency of many theories-in particular, of the theory U itself-as well as it forbids to prove…

cs.LO2023

Arithmetic as a theory modulo

Gilles Dowek, Benjamin Werner

We present constructive arithmetic in Deduction modulo with rewrite rules only.

cs.LO2023

A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions

Gilles Dowek

We present an incomplete proof synthesis method for the Calculus of Constructions which is always terminating and a complete Vernacular for the Calculus of Constructions based on t…