MANY-VALUED LOGICS
==================

Many-valued membership functions map concrete values (such as
height, weight) to a membership degree in [0..1]. Any function
will do as long as it captures the domain well. Usually there will a
flat part at the edges of the value's domain for the region where the
value definitely is or is not in the intended concept; and a straight
or sigmoid function that links the flat parts.

To evaluate complex expressions we need an algebra that interprets the
logical connectives, i.e. that decides on the valuation of
"A conjunction B" if we know the valuation of A and the valuation of
B. (And so on for all connectives foreseen by the logic's syntax.)

The concept of the triangular norm (t-norm) generalizes "conjunction"
and "intersection" as any binary operator that behaves the way we
expect (commutativity, associativity, identity element, etc).
Similarly t-conorm generalizes "disjunction"/"union" and
"residual" generalizes implication. Negation is again called negation.

A t-norm (and company) might be many-valued and continuous in [0..1].

A t-norm (and company) might be many-valued but discete. If, for
instance, a logic had valuations 0, 0.5 , 1 (a "middle" "somewhere in
between" value), a t-norm that is appropriate for interepreting this
logic should be closed in {0, 0.5, 1}.

The norms for four such algebras are:

Zadeh, aka Fuzzy:
t-norm (a and b)    min(a,b)
t-conorm (a or b)   max(a,b)
negation            1-a
redidual (a -> b)   max( 1-a , b )

Lukasiewicz:
t-norm (a and b)    max( a+b-1 , 0 )
t-conorm (a or b)   min( a+b , 1 )
negation            1-1
redidual (a -> b)   min( 1-a+b , 1 )

Goedel:
t-norm (a and b)    min(a,b)
t-conorm (a or b)   max(a,b)
negation            if a=0 then 1, else 0
redidual (a -> b)   if a>b then b, else 1

Product:
t-norm (a and b)    ab
t-conorm (a or b)   a + b - ab
negation            if a=0 then 1, else 0
redidual (a -> b)   if a>b then b/a, else 1


Although quantification would normally be expressed using t-norm
(universal) and t-conorm (existential), it is usually defined using
min, max regardless of the t-norm and t-conorm used for conjunction
and disjunction:

The expression forall R.C is the set (concept) of all instances that
have R only with members of C. So the interpretation of the expession
x : forall R.C is the degree to which all y such that R(x,y) are
members of C:

I(x : forall R.C) = forall y in D . min { I( R(x,y)->C(y) ) }

where I( R(x,y)->C(y) ) is calculated as per the algebra used.

Similarly:

I(x : exists R.C) = forall y in D . max { I( R(x,y) and C(y) ) }

Tableaux reduce the problem to a Integer Linear Programming problem
which is then passed to a solver.


Note that implication is a connective just like any other. We can
assign a valuation to (a->b), besides calculating it from the
valuations of a and b. If we know v(a->b) and v(a), we can calculate
v(b). In this sense v(a->b) is the amount of trust we place on the
assertion that a implies b.