Automated ZFC Theorem Proving with E
classification
💻 cs.LO
keywords
automatedprovingtheoremalongsideapproachaxiomatizableclasscompare
read the original abstract
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$.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.