benjishults/bitnots

prover is complete for FOL with q-limit

benjishults opened this issue · 0 comments

prover is complete for FOL with q-limit.

Any theorem provable with at most q applications of the gamma rule to each gamma formula is proved barring running out of memory.