Today I just had an insight:

Haskell Curry proposed combinatory logic as a

*logica universalis,*but it ran into inconsistency problems. (I'm trying to use fuzzy-probabilistic truth values to get around that problem, but that's a different topic.)So, in 1963 JA Robinson discovered resolution, which is really

**unification**+**propositional resolution**. Unification decides if 2 terms can be made equationally identical. Propositional resolution deals with the "calculus of thinking" at the proposition level.Combinatory logic provides a free way to compose terms via "application". I regard

**terms**as**concepts**. For example: "tall handsome guy"

is the combination of the concepts

tall ∙ (handsome ∙ guy).

Now, a few examples:

"tall handsome guy" is equivalent to "handsome tall guy";

"very tall guy" implies "tall guy"; but

"very tall guy" does not equal "tall very guy";

Thus the unification theory is modulo some special rules akin to commutativity, associativity, etc, and certain reduction rules. In other words, unification modulo a theory = "

*the calculus of concepts*".So we have a neat decomposition:

calculus of thoughts = calculus of concepts

+ calculus of propositions

+ calculus of propositions

## No comments:

## Post a Comment