Chad E. Brown

Extracting Higher-Order Goals from the Mizar Mathematical Library

2016 · arXiv (Cornell University)

Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theorem proving problems from Mizar articles that make use …

Experiments with Choice in Dependently-Typed Higher-Order Logic

2024 · EPiC series in computing

Recently an extension to higher-order logic — called DHOL — was introduced, enrich- ing the language with dependent types, and creating a powerful extensional type theory. In this paper we propose two ways how choice …