[nwfuzbqc] Proofs in games

In go 囲碁, we want to know whether a group lives.

In chess, whether a position will be a draw by perpetual check, or whether a fortress will hold indefinitely.

These are dynamic aspects of a position, testing whether a property will hold forever, as opposed to a one-time property like checkmate or group death.

What does a proof of such "forever" properties look like?  Can we automate the search for them?

Horizon effect thwarts the traditional tree search methods that evaluate game positions to finite depth.

Use Monte Carlo tree search UCT to form conjectures.

Broadly applicable to formal methods for computer programs: will this security property ever be violated?