For questions regarding the different ways to generate and verify theorems via specialized computer languages, algorithms, and other computer-aided tools.

learn more… | top users | synonyms

2
votes
1answer
267 views

Superposition calculus and equality factoring

Superposition with equality resolution and equality factoring is said to be a complete calculus for first-order logic. The purpose of equality factoring is basically to get rid of paraduplicate ...
17
votes
2answers
518 views

Is there an automated way to prove really boring elementary number theoretic results?

Motivation: I'm writing a proof, and within it, I need to prove: Conjecture: Let $p$ be an odd prime (i.e. $p \neq 2$). Let $c \geq 2$, $d \geq 1$ and $r \geq 1$. If $p^r$ divides $cd$, then $d(...