Myth Jellies wrote:The standard UR+1 or type 1 UR definition should at least allow for an unknown number of extra digits in the target cell. It should also be removing 12 from the target cell instead of placing a digit.
I don't know what the standard definition SHOULD ALLOW, I only know what this definition currently IS and this is enough to illustrate my point about the non confluence of a resolution theory containing this rule.
You may be right about what the definition of UR1 SHOULD ALLOW, I don't know and I don't want to spend time on this: uniqueness really doesn't interest me. Uniqueness in itself is not in the topics of this thread. After scanning quickly the thread you recently opened on this topic, a better place to discuss your ideas on uniqueness, I'm not convinced by anything said there and I don't plan participating in these discussions.
Myth Jellies wrote:As for your approach, I saw nothing in your rules which prohibits you from using both solved values as well as candidates in your patterns.
True. Nothing prevents it
a priori in my general concept of a resolution rule. But all the specific resolution rules I've defined, in particular all the types of chains, from the most basic and classical xy to the most elaborated nrczt-whips, don't allow this. Just check my definitions: they specify only candidates, all of which can have one and only one of 3 and only 3 statuses:
- must be present (left- and right- linking ones),
- must be absent (all those that are not specified to be present or optional),
- is optional (z- and t- candidates).
The reason for this choice is that considering decided values is useless in practice in such chains. Moreover, from a computational POV, it would lead to examining astronomically more useless partial chains.
Decided values are taken care of by elementary constraints propagation. This seems to be enough.
AFAIK, other approaches, e.g. based on graph theory, also work only on candidates.
GSF or
Red Ed, if you read this, can you confirm?
Myth Jellies wrote:I also didn't see anything which prevents you from devising or using a simple originally_solved(r, c) function.
Literally right: you didn't see it. You can't see it. It is not there. There is no such predicate (not "function") in my framework. Not only is it not there, it is not allowed.
In my framework, the (very short) list of basic predicates is closed. It is tailored to represent all and only the most elementary and direct facts one can observe on a PM. No new basic predicate is allowed.
Auxiliary predicates definable from this list may be introduced, such as the predicate describing an xy-chain[6], but from a pure logic POV, they are only shorthands for longer formulæ.
The reason is that something as "originally_solved" would be useless for all the rules I've defined (and all those I can imagine). Not only useless, but also a nuisance: it would introduce unnecessary complications.
(Indeed, before I published the 1st edition of my book, I had this predicate; I noticed I never used it; and, after analysing why, I concluded that it was useless and I eliminated it).
Using my framework, a player doesn't have to remember all his previous knowledge states (the formal logic model of PMs); he works only on the current one.
Moreover, from a player's POV, I can't see how having failed to see some UR1 at some point in time, he could remember that some UR1 was valid at that time.