72 citations · 159 across the 26 of their papers we have counts for
Showing 2026Show all
2 papers · 1 filter
cs.LO2026
Verification of a DPLL Transition System in Rocq
Julia Dijkstra, Benedikt Ahrens
We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwen…
cs.LO2026
Rzk: a Proof Assistant for Synthetic -Categories
Nikolai Kudasov, Violetta Sim, Benedikt Ahrens
Homotopy type theory (HoTT) is a type theory that allows for synthetic reasoning about -groupoids. Several proof assistants (such as Rocq and Agda) implement variants of Ho…