36 citations · 37 across the 8 of their papers we have counts for
4 papers · 1 filter
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…
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…
Interpolation and Quantifiers in Ortholattices
Simon Guilloud, Sankalp Gambhir, Viktor Kunčak
We study quantifiers and interpolation properties in \emph{orthologic}, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical…
Mechanized HOL Reasoning in Set Theory
Simon Guilloud, Sankalp Gambhir, Andrea Gilot +1
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADT) into first-order logic with ZFC axioms. We implement this in the Lisa proof assistant f…