Josef Urban

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 …

Tactic Learning and Proving for the Coq Proof Assistant

2020 · EPiC series in computing

We present a system that utilizes machine learning for tactic proof search in the Coq Proof Assistant. In a similar vein as the TacticToe project for HOL4, our system predicts appropriate tactics and finds proofs …

Property Invariant Embedding for Automated Reasoning

2019 · arXiv (Cornell University)

Automated reasoning and theorem proving have recently become major challenges for machine learning. In other domains, representations that are able to abstract over unimportant transformations, such as abstraction over translations and rotations in vision, are …