[ivan.moony]

Code

(
    ((man @x) (mortal @x)) (
        (man Socrates) (
            (man Plato) ()
        )
    )
)

It is a matter of transforming implicational logic to normal logic. `A -> ( B -> ( C -> D ) )` translates to `(A /\ B /\ C) -> D`, and `A`, `B`, and `C` are in the same context, and may interact between each other. We may use `D` as a dummy, or as something more meaningful.

[Zero]

In (a b), how would you call a and b? What are the official terms you choose? I can't choose between condition/context/rule, consequence/situation ...

[ivan.moony]

In (a b), how would you call a and b? What are the official terms you choose?

Nothing special, it's all about implications. I'd say `a` is a cause, while `b` is a consequence. Thus `a` implies `b`. But the real beauty is that we may use implication combinations to form data structures. For example, if we have a magical operator `+`, we may write the following function definition and its two use cases:

Code

(
    ( ( add ( left @x ) ( right @y ) ) ( @x + @y ) ) (
        ( add ( left 1 ) ( right 2 ) ) (
            ( add ( left 4 ) ( right 5 ) ) ()
        )
    )
)

The first meaningful line is the function definition. The second line results with `1 + 2`. The third results with `4 + 5`. Try to copy and paste this example into implika test suite and see what happens to `ForeChain` property. Remember, implika is a very simple variant of implicational logic, but we have just been doing math with it.

Thank you for reminding me of this project, I put it aside in a favor of super-duper-logic-able-doing-parser esperas. Nevertheless, I might finish implika one day, I'd still like to simplify different contexts parent-child interaction.

[Zero]

Yes I can see that it can represent data structures. Actually, I was working on an expansion of consnets, in OrientDB (see the other thread?) Trying to capture the essence of things, I came to a point where I introduced "truth" and "context" for handling first order logic. Implika popped up in my mind, I reread it, and found it would fit perfectly here.

First, I still need a way to make things move, I don't have rules in my system yet, and you know how much I love minimalism. But I also need to express contexts. I feel contexts is a very primitive concept.

You probably remember that consnet is all about pairs. Pairs is enough to create everything else. But then, there's a schema that comes again and again, which is [LinkType [Left Right]], so I thought that "type" was primitive enough to deserve its own existence. Then, following OpenCog, I wondered about truth and context, and the next step was to add wildcards too, because who doesn't like patterns, right?


Now, with Implika, I think "truth" and "context" are actually the very same thing. Maria Keet says: What matters in logic is not the actual truth of a statement, but rather the relationship between the truth of one statement and that of another.

[ivan.moony]

Be careful if you use only implications, I'm still uncertain about them representing sequences. There was something wrong about it, but I forgot the solution. In logic, if we have `( ( ( A -> B ) -> C ) -> D )`, and if we say `C` in the top context, then from `C` follows `D` without even mentioning `A` and `B`. I don't know how to feel about this logical property, but it seems a nasty one.

About types, you can get away without special operator by demanding the whole expression to be tautology (it is said valid). If the top expression is `SomeA -> SomeB`, then if we consider it a tautology, then `SomeA` is of type `SomeB`. However, expressions constituting `SomeA` and `SomeB` may be only satisfiable, making a room for some needed acrobatics. The third case is contradiction treatment, which may be reported as an error, but they (Gödel) say that that kind of system is then not complete. For a while now, I don't believe them anymore. I suppose there may be multiple onion skin metalayers of which the above may be valid or satisfiable (in contrast to contradictory), while retaining ability to express lower system which may be contradictory if we want.

[Zero]

Man, this baby needs a little love. To me, Implika might be one of your greatest works.

And what about backward chaining? Do you think it's possible to enhance it?

[ivan.moony]

I think if all logical operators could be expressed in implika, then `( ( A -> B ) /\ B ) -> A` simulates backward chaining without any special treatment. Try to paste the following example in implika test suite:

Code

(
    (
        ( @x -> @y ) (
            ( ( fore @x ) @y ) (
                ( ( back @y ) @x ) ()
            )
        )
    ) (
        ( rains -> wet ) ()
    )
)

After drawing conclusions, expression `rains -> wet` should in ForeChain property have forward and backward chained cause and consequence.

However, to extract correct results from `fore rains` and `back wet` some crazy stunts with contexts are required, which would be more easily solved with still unimplemented hierarchical contexts.

[Zero]

Ok, so to avoid crazy stunts, would you need to expand the model? Or would it be more like changing the algo?

[ivan.moony]

It would be an algo adjustment. No additional syntax, just a few loops rearrangements if I remember correctly (I was about to do this before something else attracted my attention). But I think I'd need at least a week to remember what I was doing and to plan things up before making the adjustments (not to inject bigger amounts of code than really needed - I want to keep it below 200 lines of Javascript).

As a motivation, I think we can expect example implementation of the entire Hilbert calculus in about 15-20 lines of more readable implika code instead of the current unnecessary mess among 47 lines.

[Zero]

I think it's worth it, especially if it is a building block of a bigger project like e-Teoria.

One interesting improvement could be the addition of a syntax for inline comments. I suggest "double quotes anywhere", or [square brackets], being ignored by the parser (together with a good-practice section explaining how to use them). Because since pairs can be conceptually anything, readability of Implika code is currently absolutely awful!!

You're the master of Implika, but while I'm at it, I find @var syntax not so pretty. May I suggest <var> or var? instead? Sorry, probably not my business...

[ivan.moony]

You're the master of Implika, but while I'm at it, I find @var syntax not so pretty. May I suggest <var> or var? instead?

I have to admit, `<var>` looks much prettier to me too. I also kind of like capital letters denoting variables, while lower letters denoting constants.

[Zero]

Yes, I thought about Uppercase first letter too, à la Prolog.

About comments, having them between double quotes is unusual, but this is how Smalltalk does it for example. It seems reasonable to me. One way or another, I think comments are very important in a language, you should choose a syntax for them.

Code

( "one meaningful context"

    (("pattern" man <x>) ("template" mortal <x>)) (

        ("starting from" man Socrates) ()
    )
)

Another question. I would expect the state after inference-step to be represented in the same format. Currently, a ForeChain key is added, with the result as an array. This breaks the head/tail format. How do we represent the result of the inference in Implika syntax?

[krayvonk]

One funny thing I think about symbolic logic, is the "framework" thats running your system could just be more symbolic logic.  very confusing topic.
If anyone cracks how to do it really good,  it puts hairs on your chest.

I love that first picture,  why dont you put symbolic logic in a fractal!   Its like that thing I just said, the system running the system, or it would be like "10 people with 10 forks with 10 steaks with 10 blobs of ketchup with 10 little bits of parmesan cheese particles."  - couldnt go more micronicly setted than that in this case.

[Zero]

He did
https://aidreams.co.uk/forum/index.php?topic=12849.msg60380#msg60380

[ivan.moony]

About comments...

Well, there is already a way to state `(pattern @a) @a`, and later to use it as `pattern (man @x)`, just to increase verbosity. But general comments will certainly be taken under consideration.

I would expect the state after inference-step to be represented in the same format. Currently, a ForeChain key is added, with the result as an array. This breaks the head/tail format.

Sounds extraordinary. I should give it a try.

How do we represent the result of the inference in Implika syntax?

Nohow. Inference particles are just there in forechain to interact with other initial/forechain particles, making new forechain particles.

[EDIT]
continuing in the next post