# Automated ZFC Theorem Proving with E

## TL;DR

This paper presents an approach for automated theorem proving in complex set theories like ZFC using the E prover, and compares proof search results between NBG and ZFC.

## Contribution

It introduces a novel method for automated reasoning in non-finitely axiomatizable set theories and implements it within the E theorem prover.

## Key findings

- Proof search in NBG differs from ZFC
- Automated reasoning in ZFC is feasible with the proposed approach
- Comparison highlights strengths and limitations of each set theory in automated proof search

## 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$.