ATP-proofs (Automated Theorem Prover - Proofs)
This is a collection of example proof scripts to help any new person learn proving maths using computer programs. Many of these are very basic for now but I'll try to add complex examples as soon as I learn more.
Currently the set of examples target COQ as the interactive theorem prover but I will try to translate them for other proof assistants too.
The basic/ part contains the super basic ideas and fundamentals of working of a given ATP.
This includes its own used ways and tactic systems.
| Proofs | Coq | Isabelle |
|---|---|---|
| De Morgan's Law | Yes | No |