[ivan.moony]

Been on a mind journey through logic land last few days and I report results here, as I promised.

a logic jurney

I have always thought that we internally think in a language of logic. I don't know is this is the real truth, but it is possible to build complex knowledge particles by a subset of logic operators that includes: "&" (and), "|" (or) and "->" (implies). As we will see, we can get away without "~" (not) in top level representation, although it is necessary to be used internally, for internal calculations. I will not bother you with low level deduction algebra that hides behind the theory, but patterns I will show here are rather intuitive, while intuition follows more complex calculations done under the hub.

In further examples, for a start, we will use our own language to define knowledge. Our language will be a combination of "=>", "<=", ";" and "," operators in a following way:

Code

Object => (Property1, Property2, ...)

while each property can stand for another object. If we want a property to contain multiple objects, we write:

Code

Property => (Object1; Object2; ...)

Of course, we can combine our properties and objects to form complex expressions. Then we will convert expressions of our language to logic expressions, thus preparing them for later use. After converting to logic expressions, we can run proof inference to deduce wanted knowledge. We will know in advance what we need and we will show how to reach what we need.

deduction
We start from preparing existing data for later use. We want our data to be structured in a way that gives us the possibility to extract data fragments when we need them. We will be able to state an object with a number of properties, and to reach values of object properties by deduction.

Here is our first example of defined "Helicopter" object:

Code

Helicopter => (
    Engine => OttoMotor,
    ScapeType => (
        SkyScape => (
            MaximumAltitude => 4000m,
            StormResistance => Low
        )
    ),
    Use => (Transport; Cargo)
)

The task we want to accomplish is when we write something like:

Code

Use

we want our logic engine to automatically deduce

Code

Transport
Cargo

which are values stored under "Use".

In order to do this, we have to convert  the whole tree to its logic equivalents in the following way. First, every:

Code

A => (B; C; ...)

we have to split into:

Code

A => B
A => C
A => ...

and every:

Code

A => (B, C, ...)

we have to split into the same:

Code

A => B
A => C
A => ...

Further, because of internal properties of logic implication operator, to get wanted behavior of a proof finder underneath, we have to replace each expression of:

Code

A => (B => (C => (...)))

by:

Code

A -> B
B -> C
C -> ...

Now, that we have converted the whole tree to classical logic implications, we can run classical logic proof engine to do deduce data we need. So, when we assert an example from the start:

Code

Use

the proof finder asserts the following set of truths:

Code

Transport
Cargo

which in turn is exactly what we needed at the beginning.

What is really happening is that we get deduced all tree nodes below (but not above!) wanted node in a flat list format. This list can later be used for reaching data, and assigning it to wanted symbols. For example, we can write:

Code

X => Engine

Afterwards, when we state:

Code

X

then among others, the following truth pops up:

Code

Ottomotor

We have shown how we can filter results by deducing from properly structured data and how to assign those results to other symbols. The key thing is that both "A => (B, C)" and "A => (B; C)" convert to a pair of "A -> B" and "A -> C". What logic proof engine does afterwards is somewhat intuitive.

induction
We continue with recognizing data. Now we want our data to be structured in a way that gives us the possibility to inductively conclude what we are expressing. We will be able to state a number of properties, and to automatically conclude what object the properties describe.

Here is our next example of fully defined "Vehicle" object, needed for later recognition:

Code

Vehicles <= (
    Engine <= (OttoMotor; Helix; Jet),
    ScapeType <= (
        SeaScape <= (
            HydroPlaning <= (Yes; No)
        );
        GroundScape <= (
            ContactType <= (Wheels; Magnet)
        );
        SkyScape <= (
            MaximumAltitude <= Integer,
            StormResistance <= (Low; Medium; High)
        )
    ),
    Use <= (Tourism; Transport; Cargo)
)

The task we want to accomplish is when we write something like:

Code

OttoMotor, Wheels, Cargo

we want our logic engine to automatically induce that we write about "Vehicle".

In order to do this, we have to convert  the whole tree to its logic equivalents in the following way. First, every:

Code

A <= (B, C, ...)

we have to convert to:

Code

A <= (B & C & ...)

Then every:

Code

A <= (B; C; ...)

we have to split to:

Code

A <= B
A <= C
A <= ...

Further, because of internal properties of logic implication operator, to get wanted behavior of a proof finder underneath, we have to replace each expression of:

Code

A <= (B <= (C <= (...)))

by:

Code

A <- B
B <- C
C <- ...

where "A <- B" is the same as "B -> A", only written in reverse order.

Now, that we have converted the whole tree to classical logic implications, we can run classical logic proof engine to do deduction which in fact performs total induction on given example. So, when we assert an example from the start:

Code

OttoMotor, Wheels, Cargo

proof finder asserts the following truth:

Code

Vehicle

We have shown how induction can be performed using logical operators. The main intuitive thought over the complex logic layer is: to conclude A from "A <= (B; C; D)", it is enough to recognize any of B, C or D; to conclude A from "A <= (B, C, D)", we should recognize all of B, C and D. Former expression is called a sort of disjunction, and later a sort of conjunction. Those two are enough to inductively recognize complex structures from simple facts.

I'm still investigating functions over logical operators. They could be called a sort of higher order constructs.

[Edit]: done... I thought it would be somewhat complicated, but it's simple, really...

functions
Functions are really no mystery, once you realize that they bind specific results to different parameter combinations. All we have to do is to bind those pairs by implication operators and to connect different cases by "&" operator under the function name:

Code

And -> (
    (Left -> True & Right -> True)   -> True &
    (Left -> True & Right -> False)  -> False &
    (Left -> False & Right -> True)  -> False &
    (Left -> False & Right -> False) -> False 
)

This way arranged semantic table can be reached by the following proposition:

Code

And -> (Left -> True & Right -> True)

Having that stated, after some proof calculation, we get the following proposition as a result:

Code

And -> True

which is exactly what we want. Moreover, we can use this style of defining functions for higher order function use (higher order functions either taking other functions as parameters, either returning them as a result):

Code

X -> And
X -> (Left -> False & Right -> True)

We stored function And into a higher order variable X and later called X with some parameters. Afterwards, we automatically get

Code

X -> False

as a result proposition. Works.

It is really simple and easy, and intuitive enough to understand it without being an expert in the field of logic. Folks, logic rocks

[Zero]

I did not understand how we translate ...<=... to ...->...

But I understood this:

We have shown how induction can be performed using logical operators. The main intuitive thought over the complex logic layer is: to conclude A from "A <= (B | C | D)", it is enough to recognize any of B, C or D; to conclude A from "A <= (B & C & D)", we should recognize all of B, C and D. Former expression is called a sort of disjunction, and later a sort of conjunction. Those two are enough to inductively recognize complex structures from simple facts.

I think that's how we "call" objects in our minds. We never think "I need the key of my car", we rather think "I need the little metal thing in my pocket". We call objects by their properties. This means that when we memorize stuff (by association), we don't associate objects, we associate their properties.
What do you think?

[ivan.moony]

I did not understand how we translate ...<=... to ...->...

Yes, I admit it's a bit messy and I don't like it either, but it works somehow. There might be other ways, I'll try to find them. At least I like the way deduction and functions are written.

To recognize a key it is enough to have this construction:

Code

Key <- (Size <- Little & Appearance <- Metal & Position <- Pocket)

But later, to reach specific properties of the key, we have to put it this way also:

Code

Key -> (Size -> Little & Appearance -> Metal & Position -> Pocket)

[Zero]

Yes, so I looked at Wikipedia's article on logical connective.

To be able to recognize a key and reach specific properties, we would need equivalence, am I right?

The interesting part is the key recognition. It would be great to automate the creation of structures like:

Code

Key <- (Size <- Little & Appearance <- Metal & Position <- Pocket)

It's like having a list of varying boolean variables, observing their variations, and deducing their logical connections. Is it the Boolean satisfiability problem?
I believe spydaz is working on it, but I may be wrong.

[ivan.moony]

Is it the Boolean satisfiability problem?

Might be, I'm not sure what kind of automation would it be. Once I thought of randomly imagining of new formulas, then inductively checking if they satisfy the model. Then yes, it would be just it.

(I have rewritten induction paragraph, it is a little bit more concise now, but not much. I also asserted that "A.B.C" reaching from deduction paragraph is somewhat like "A & B & C" in logic language.)

[Zero]

I don't know if it's BSP...

I'll try to explain what's on my mind:

Imagine we have an input like this

Code

	A B C D E F G H
	1 0 1 1 0 1 0 1
	1 0 1 0 1 1 0 1
	0 0 1 1 0 0 0 0
	1 0 0 1 1 1 0 0

It would be nice to be able to detect automatically that H = A and C

[ivan.moony]

I don't know if it's BSP...

I'll try to explain what's on my mind:

Imagine we have an input like this

Code

	A B C D E F G H
	1 0 1 1 0 1 0 1
	1 0 1 0 1 1 0 1
	0 0 1 1 0 0 0 0
	1 0 0 1 1 1 0 0

It would be nice to be able to detect automatically that H = A and C

Zero, you are a genius

Unfortunately, that's not such an easy task. You have to enumerate all combinations of ("A = B and C", "A = B and D", "A = B and E", ...) Then you have to check them, one by one, does they hold for given model (that table). That checking is in fact the induction (each line in the table is an induction element that needs to be checked. If they all pass, you have a total induction conclusion). When you come to "H = A and C", it passes and you want to save it to memory for later use (deduction or something).

And then you move to more complicated combinations like "A = (B and C) or not D", which gives us combinatorial explosion up to near infinite number of combinations (or exactly infinite if we deal with infinite sets like natural numbers). To speed it up, we could use genetic algorithm (GA) that combines fragments of formulas that passed checks in the past. GA doesn't reduce the number of combinations, but it helps to extract those with a higher probability for success.

I don't know what is that called, but it is (by my opinion) the very essence of intelligence: being able to imagine new formulas, checking and remembering them for later dumb tasks like deduction or recognition by induction. It is definitely an important part in building AGI. I'd call it a creativity process.

[Zero]

And then you move to more complicated combinations like "A = (B and C) or not D", which gives us combinatorial explosion

Well, what if we don't move to more complicated combinations?

We could just add another letter I, then J, K, L...

Instead of A = (B and C) or not D

We would have
A = J or K
J = B and C
K = not D

Then we can detect things easily. Looks like Logical Neurons

[ivan.moony]

I've updated the original article from the first post to match the new insights. Deduction and induction paragraphs are now updated to be visibly oppositely analogous each to other. The function paragraph is not changed.

[8pla.net]

Imagine we have an input like this

Code

	A B C D E F G H
	1 0 1 1 0 1 0 1
	1 0 1 0 1 1 0 1
	0 0 1 1 0 0 0 0
	1 0 0 1 1 1 0 0

It would be nice to be able to detect automatically that H = A and C

Zero, you are a genius


Unfortunately, that's not such an easy task. You have to enumerate all combinations of ("A = B and C", "A = B and D", "A = B and E", ...) Then you have to check them, one by one,

We could easily have machines assist with that task...

Code

[0] 0:A 1:B 2:C 3:D 4:E 5:F 6:G 7:H 
[1] 0:1 1:0 2:1 3:1 4:0 5:1 6:0 7:1 
[2] 0:1 1:0 2:1 3:0 4:1 5:1 6:0 7:1 
[3] 0:0 1:0 2:1 3:1 4:0 5:0 6:0 7:0 
[4] 0:1 1:0 2:0 3:1 4:1 5:1 6:0 7:0 

Code

0, 0=>A, 1=>B, 2=>C, 3=>D, 4=>E, 5=>F, 6=>G, 7=>H, 
1, 0=>1, 1=>0, 2=>1, 3=>1, 4=>0, 5=>1, 6=>0, 7=>1, 
2, 0=>1, 1=>0, 2=>1, 3=>0, 4=>1, 5=>1, 6=>0, 7=>1, 
3, 0=>0, 1=>0, 2=>1, 3=>1, 4=>0, 5=>0, 6=>0, 7=>0, 
4, 0=>1, 1=>0, 2=>0, 3=>1, 4=>1, 5=>1, 6=>0, 7=>0,

Code

$Zero=array(
array(0, "A", "B", "C", "D", "E", "F", "G", "H", ),
array(1, 1, 0, 1, 1, 0, 1, 0, 1, ),
array(2, 1, 0, 1, 0, 1, 1, 0, 1, ),
array(3, 0, 0, 1, 1, 0, 0, 0, 0, ),
array(4, 1, 0, 0, 1, 1, 1, 0, 0, ),
);

[ranch vermin]

I read it briskly because im presuming its not much different than a whole lot of ordinary programming, but its getting extracted off the sensor right?

In my mind, a ga doesnt enhance this,  but this actually REPLACES a ga.

So, a ga is an anealing of mutations,  so we build up of what we last knew, given our last things we did.
This has the issue that we cant develop anything but nearness to what we last did.

This is a "pattern self development"   In other words, it aint new, but we are compounding on what we last knew, EXACTLY the same as a GA basing its new movements off its old movements in a simple hybriding fashion,  but this is logical deduction instead.

And its got to be better.

[ivan.moony]

Yes, so I looked at Wikipedia's article on logical connective.

If you like logic, you might be interested in propositional logic and resolution rule.

I do all calculations on paper (more precisely in text editor) by the resolution rule. It is complete method, so it concludes everything that can be concluded from a set of formulas.

[Edit] this is how a fragment from my workbook looks like:

Code

*Bool <- (*True | *False)
@Any <- (
----------------------------- implies from / follows from / specifies from ---- reduces to / specifies to / applies from
-- symbols contain objects?
    *And <= (
        (
            Bool <= (*Left <= Bool, *Right <= Bool)
        ) <-> (
            (Bool <- True)  <- (Left <- Bool <- True,  Right <- Bool <- True)  &
            (Bool <- False) <- (Left <- Bool <- True,  Right <- Bool <- False) |
            (Bool <- False) <- (Left <- Bool <- False, Right <- Bool <- True)  |
            (Bool <- False) <- (Left <- Bool <- False, Right <- Bool <- False)
        )
    )
)
fact <- (
    (p <- @Num) <- (
        @Num -> (
            @Case -> (
                (@p == 0) -> 1 |
                (@Else)   -> @p * (@fact -> (@p - 1))
            )
        )
    )
)

-----------------------------------
B <- B1
A <- B <- C
-----------------------------------

Metatheory, MetaLogic -:- :- -: specifies from / specifies to ; induces from / deduces to
And <- (
    (
        (Bool, Bool) <- Bool
    ) -> (
        (True, True)   -> True |
        (True, False)  -> False |
        (False, True)  -> False |
        (False, False) -> False
    )
)
Result <- (@And -> (True, False))
-----------------------------------
Bool <- (True | False)
¬ (True | False) | Bool
¬True | Bool
¬False | Bool
---------------------------
a <- Bool
¬Bool | a
¬True | a
¬False | a

a -> True
¬a | True
---------------------------
(a <- Bool) <-> (a <- True)
---------
¬(¬Bool | a) | (¬True | a)
Bool | ¬True | a

(¬Bool | a) | ¬(¬True | a)
¬Bool | a | True

---------------------------
*******************
((a | b | c) -> (p | q | r)) -> (u | v | w)
*******************
    ~((~a & ~b & ~c) | p | q | r) | u | v | w
    ((a | b | c) & ~p & ~q & ~r) | u | v | w

*******************
(a | b | c) -> ((p | q | r) -> (u | v | w))
*******************
    ~(a | b | c) | (~(p | q | r) | u | v | w)
    (~a & ~b & ~c) | ((~p & ~q & ~r) | u | v | w)

*******************
x <- ((a <- Bool) -> (a -> True | a -> False))
*******************
    x | ¬(¬(a | ¬Bool) | (¬a | True) | (¬a | False))
    x | ((a | ¬Bool) & ¬(¬a | True) & ¬(¬a | False))
    x | ((a | ¬Bool) & a & ¬True & a & ¬False)
    -
    x | a | ¬Bool
    x | a 
    x | ¬True
    x | ¬False

*******************
(a <- Bool) <-> (a -> True)
*******************
    ¬(¬Bool | a) | (¬a | True) // (a <- Bool) -> (a -> True)
    Bool | ¬a | True
    ¬a | True

    (¬Bool | a) | ¬(¬a | True) // (a <- Bool) <- (a -> True) 
    ¬Bool | a
    ¬Bool | a | ¬True

*******************
(a <- Bool) <-> (a -> True | a -> False)
*******************
    ¬(¬Bool | a) | (¬a | True) | (¬a | False)  // (a <- Bool) -> (a -> True | a -> False) 
    Bool | ¬a | True | False
    ¬a | True | False

    (¬Bool | a) | ¬((¬a | True) | (¬a | False)) // (a <- Bool) <- (a -> True | a -> False) 
    (¬Bool | a) | (¬(¬a | True) & ¬(¬a | False)) 
    (¬Bool | a) | (a & ¬True & ¬False)

*******************
(a <- Bool) <-> (a <-> True | a <-> False)
*******************
    ¬(¬Bool | a) | (((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False))) // (a <- Bool) -> (a <-> True | a <-> False) 
    (Bool & ¬a) | (((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False)))
    (Bool & ¬a) | (((¬a | True | ¬a | False) & (a | ¬True | ¬a | False) & (¬a | True | a | ¬False) & (a | ¬True a | ¬False)))
    (Bool & ¬a) | ((¬a | True | False) & (a | ¬True | ¬False))
    -
    Bool | (¬a | True | False)
    Bool | (a | ¬True | ¬False))
    ¬a | True | False

    (¬Bool | a) | ¬(((¬a | True) & (a | ¬True)) | ((¬a | False) & (a | ¬False))) // (a <- Bool) <- (a <-> True | a <-> False) 
    (¬Bool | a) | (¬((¬a | True) & (a | ¬True)) & ¬((¬a | False) & (a | ¬False)))
    (¬Bool | a) | ((¬(¬a | True) | ¬(a | ¬True)) & (¬(¬a | False) | ¬(a | ¬False)))
    (¬Bool | a) | (((a & ¬True) | (¬a & True)) & ((a & ¬False) | (¬a & False)))
    (¬Bool | a) | ((a | True) & (¬a | ¬True) & (a | False) & (¬a | ¬False))
    -
    (¬Bool | a) | a | True
    (¬Bool | a) | a | False

------------
(a <- Bool) <-> (a <- (Bool <- True))
---------
¬(¬Bool | a) | (¬(¬True | Bool) | a)
(Bool & ¬a) | ((True | a) & (¬Bool | a))
Bool | True | a

(¬Bool | a) | ¬(¬(¬True | Bool) | a)
¬Bool | a | ¬((True & ¬Bool) | a)
¬Bool | a | ((¬True | Bool) & ¬a)
---------
True
Bool | a
True | a

(Bool <-> True) | a
((¬Bool & True) | (Bool & ¬True)) -> a
-----------------------------------
GS <- CT <- (W | M)
gs | ~(ct | ~(w | m))
gs | (~ct & (w | m))
gs | ~ct
gs | w | m
-
~ct | w
-
gs | ~ct
ct | ~w


-----------------------------------
And -> (
    (Left -> True & Right -> True)   -> True |
    (Left -> True & Right -> False)  -> False |
    (Left -> False & Right -> True)  -> False |
    (Left -> False & Right -> False) -> False 
)
~And | (
    ~((~Left | True) & (~Right | True)) | True |
    ~((~Left | True) & (~Right | False)) | False |
    ~((~Left | False) & (~Right | True)) | False |
    ~((~Left | False) & (~Right | False)) | False 
)
~And | (
    (~(~Left | True) | ~(~Right | True)) | True |
    (~(~Left | True) | ~(~Right | False)) | False |
    (~(~Left | False) | ~(~Right | True)) | False |
    (~(~Left | False) | ~(~Right | False)) | False 
)
~And | (
    ((Left & ~True) | (Right & ~True)) | True |
    ((Left & ~True) | (Right & ~False)) | False |
    ((Left & ~False) | (Right & ~True)) | False |
    ((Left & ~False) | (Right & ~False)) | False 
)
~And | (
    ((Left & Right) | (Left & ~True) | (~True & Right) | (~True & ~True)) | True |
    ((Left & Right) | (Left & ~False) | (~True & Right) | (~True & ~False)) | False |
    ((Left & Right) | (Left & ~True) | (~False & Rigth) | (~False & ~True)) | False |
    ((Left & Right) | (Left & ~False) | (~False & Right) | (~False & ~False)) | False
)
-----------------------------------
a -> (b -> (c -> (d -> e)))
~a | ~b | ~c | ~d | e

-----------------------------------
(((a -> b) -> c) -> d) -> e
~(~(~(~a | b) | c) | d) | e
((~(~a | b) | c) & ~d) | e
((a & ~b) | c) & ~d) | e
(((a | c) & (~b | c)) & ~d) | e
-
a | c | e
~b | c | e
~d | e
-----------------------------------
((a -> b) -> c) -> d)
~((a & ~b) | c) | d
((~a | b) & ~c) | d
-
~a | b | d
~c | d
-----------------------------------
(a -> b) -> c
-
a | c
~b | c
-----------------------------------
a -> b
-
~a | b
-----------------------------------
a => b & c
a -> b
a -> c
-----------------------------------
a <= @Bool => True
(a => Bool) => True

a <= (@Bool => True)
a => (@Bool => True)
-----------------------------------
~a | b
~b | c
~c | d

hehe, i must be insane to do this

[Zero]

You surely are, just like the rest of us   

I was thinking about this:

Unfortunately, that's not such an easy task. You have to enumerate all combinations of ("A = B and C", "A = B and D", "A = B and E", ...) Then you have to check them, one by one

The task would be easier with an attention system. If the program can focus on certain parts (for example, only A, B, C, and H), then it can detect logical links faster.