Skip to main content

Use this tag when a Proof Assistant is relying on automation. The automation can be internal or external to the proof assistant. An typic external form of automation is an automatic theorem prover. Consider also using the tag atp if that applies.

A gentle introduction to automated reasoning (ref)