6 citations · 6 across the 6 of their papers we have counts for
3 papers · 1 filter
Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
Johannes Niederhauser, Chad E. Brown, Cezary Kaliszyk
Dependent type theory gives an expressive type system facilitating succinct formalizations of mathematical concepts. In practice, it is mainly used for interactive theorem proving…
Experiments with Choice in Dependently-Typed Higher-Order Logic
Daniel Ranalter, Chad E. Brown, Cezary Kaliszyk
Recently an extension to higher-order logic -- called DHOL -- was introduced, enriching the language with dependent types, and creating a powerful extensional type theory. In this…
A Formal Proof of R(4,5)=25
Thibault Gauthier, Chad E. Brown
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The author…