2019/02/03 by Hester, John
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1902.00818
I introduce an approach for automated reasoning in first order set theories that are not finitely axiomatizable, such as ZFC, 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 NBG with those of ZFC.