I thought it might be good to look at a couple of examples from the user’s POV and think about how to reverse engineer how to achieve it.
Each of these would be particular “entities”, equivalent to the constructions in Zendo, for which a given rule could be judged to be satisfied or not.
A model of the entity construction could be a tree with vertices representing objects (including “platonic?” properties) and edges representing relations. Some relations could imply “computed” reciprocal and/or transitive relations (eg contains, left of). See the images and diagrams as examples.
Once you define the valid nodes and relations for
a type of entity, you need a way to test the satisfaction of a rule against a particular entity, as well as a way to generate some that satisfy as well some that don’t satisfy a rule.
This is similar to your FOL puzzles, except that the rule is not used to select particular nodes in the tree but rather to just describe some part of it. In the rule-deduction game it would be a common valid descriptor for a set of generated entities, out of all the possible entities for that entity type.
Would an AST representation of the rule be best model for using when testing if a particular entity satisfies it?
Another task is to hook up interfaces for rule design by the user and rule communication to the user. These should probably start out very simple and gradually increase in complexity to match rule complexity (from toggle buttons to something like Scratch block coding and finally progressing to full-blown FOL syntax?), since the idea is to step up the user’s skills.

