Automated ZFC Theorem Proving with E
Logic in Computer Science
2019-02-05 v1
Abstract
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 automated theorem proving software E. I then compare the results of proof search in the class based set theory with those of .
Cite
@article{arxiv.1902.00818,
title = {Automated ZFC Theorem Proving with E},
author = {John Hester},
journal= {arXiv preprint arXiv:1902.00818},
year = {2019}
}