Back to Prolog and other formal systems, there actually is some body of work devoted to this kind of reasoning. LTL is a great example (see the link for more).

Basically, these systems work on formal systems that are based on states. Given you are in a state, prove that the system will eventually get to some other state or will never arrive at some state. These kinds of temporal propositions allow for a programmer to prove that their system will never arrive at a certain undesirable state or will always reach a desirable one.

A practical example of this is the Line 14 of the Paris Metro, if I recall right. The whole software for it was written in a formally verifiable language, so there is an actual (computer generated) mathematical proof that the metro line has no bugs, all based on this notion of forward/backward tracking state changes in the system