Logic Unification in Trinary Logic

Im still workin on making the logic programming language of my dreams. Right now I have to get some sort of unification working, but Im using trinary logic so its been a bit of an adventure. Prolog doesn't have real negation so it really manages to sidestep alot of actual work. Informally in my logic system, called Llull, a statement has three possible truth states: 0 = No, 1 =Iono, 2 = Yes.

Yes and No are basically like True or False. Iono is much different. Since negation is allowed in Llull, determining wether a model implies something is an NP Hard problem. My unification isn't an exhaustive search, therefore, for hard problems, Llull will just throw its hands up in the air and say "iono and i don't care to actually figure it out". Iono means that either theres no data about the thing you asked about, or that it just can't find it.

Anyway, traditionally And, Or, and Not have been defined for trinary as:

• And(s1,s2) = min(s1,s2)
• Or(s1,s2) = max(s1,s2)
• Not(1) = 1
• Not(0) = 2
• Not(2) = 0

If you check, these definitions make tons of sense. But to see why they really arent sufficent for my purposes maybe I should cover my unification algorithm. My unification algorithm works by breaking up statements in this manner (where s1, s2, s3 are all Llull statements) :

• s1 -> And(s2, s3) if And(s1->s3, s2 ->s3)
• s1 -> Or(s2, s3) if Or( s1->s3, s2->s3)
• s1 -> Not(s3) if Not(s1->s3)

Rough Example:

Sean is a CS/Math Major -> Sean Studies CS And Sean Studies Math
iff
Sean is a CS/MathMajor -> Sean Studies CS And Sean is a CS/Math Major -> Sean Studies Math

Seeing this, it would be tempting to believe in rules such as:

• And(s1, s2) -> s3 if Or(s1->s3, s1->s3)

This would be the case if we didnt' have Not, which is the source of all our No/0 values. But If we consider this case:

• Suppose s1->s3 = 1. That is, Statement 1 doesn't tell us wether Statement 2 is True. Suppose s2 -> s3 = 0. That is, Statement 2 tells us that Statement 3 is False.
• Our algorithm gives us the wrong answer. It gives 1 when it should give 0.

Clearly what is needed is a function like Or and one thats like And. I figured out what they should be and named the Or substitute Kind, the And substitute Cruel. I really don't know how the names came up in my head, they just did. They names just seem to fit well somehow.