3 papers
cs.FL2023
Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning
John Hester, Briland Hitaj, Grant Passmore +3
Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-expon…
math.HO2021
Metaphysics in Mathematics
John Hester
The purpose of this project is to outline various philosophies on the metaphysics of mathematics that have been prominent since the time of Cantor, highlighting some biographical a…
cs.LO2019
Automated ZFC Theorem Proving with E
John Hester
I introduce an approach for automated reasoning in first order set theories that are not finitely axiomatizable, such as , and describe its implementation alongside the automa…