36 citations · 37 across the 8 of their papers we have counts for
Showing 2026 · cs.LOShow all
2 papers · 2 filters
cs.LO2026
Orthologic for SAT Solving
Vladislas de Haldat, Simon Guilloud, Viktor Kunčak
We present a new algorithm for deciding formula entailment in orthologic (a sound approximation of classical logic) that avoids the costly preprocessing phase of prior implementati…
cs.LO2026
Are Dependent Types in Set Theory Feasible?
Yunsong Yang, Simon Guilloud, Viktor Kunčak
Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, wi…