# Introduction A lot of Prolog programming is about stating the obvious and having the system figure out the rest. This usually means writing facts and predicates that encode our knowledge of “the world”. However, sometimes what we know isn’t a universal fact, but a runtime invariant that can only be defined in the context of a predicate’s execution. In this article I want to demonstrate the usefulness of explicitly expressing some of those invariants at the code level.

This is a test post. I test latex inline formula here: $x = a_1^n + b_2$ and block formula here: \[ sum = \sum_{c=1}^{n}x^n \]