The initial board is the starting axiom, and you want to prove (derive) a completely filled board. It's easier to think model-theoretically about games like thi

The initial board is the starting axiom, and you want to prove (derive) a completely filled board. It's easier to think model-theoretically about games like this, but I've found that as I learn a logic puzzle over time, I build up a repertoire of rules I can apply. (In fact, for puzzles-masyu.com, I have a sound and mostly complete set of rules in my mind for the Medium difficulty and periodicals.) The application of these rules typically produces a linear proof, because we augment the board state sequentially. But that's a human limitation, not a formal one. Since any rule that could be applied always can be applied (so long as there's a unique solution!), if you notice you can do two things from the same proof state, you can imagine a "rule of concurrency" that joins the results from multiple prior rules. This kind of structure is even clearer in Picross 3D: Round Two, which has two different colors that interact very loosely. You can often work purely in one color, then switch to working on the other color, and go back and forth -- it's like you're interleaving two concurrent actors both collaborating on the same object. A purely semantic perspective doesn't really lend itself to this observation -- but when you've built up a corpus of rules, it's very obvious which rules are color-local and which require a more global view to progress.