# Difference between revisions of "ICMS 2014 session on automated proofs by induction"

In many contexts one proves properties of the form ${\displaystyle \forall n\in \mathbb {N} ~P(n)}$. For instance, formal verification of software proves safety properties of the form “for any number of program steps, the output satisfies the specification”.
In easy cases, ${\displaystyle P(n)}$ can be proved by induction: ${\displaystyle P(0)}$ holds and ${\displaystyle P(n)\Rightarrow P(n+1)}$ holds for all ${\displaystyle n}$. In most cases, however, one must invent some property ${\displaystyle Q}$ that is “inductive” (${\displaystyle Q(0)}$ holds and ${\displaystyle Q(n)\Rightarrow Q(n+1)}$ holds for all ${\displaystyle n}$) and such that ${\displaystyle Q(n)\Rightarrow P(n)}$ holds. In software verification, such a property is called an “inductive invariant”.