ngeiswei commented 9 years ago

The backward chainer needs to know the structure of its implicand in order to select the applicable rules of a target. The problem is that given the way rules are currently represented, the implicand does not need to be explicit. Given the following format

BindLink
   AndLink
      <Implicant>
   <Implicand>

Implicand is usually hidden in an ExecutionOutputLink like

ExecutionOutputLink
   "scm:compute-the-implicand"
   ListLink
      ARG1 ... ARGn

Currently the backward chainer looks at ARG1 to ARGn to guess the implicand, but nothing guaranties that this guess is correct, ARG1 to ARGn may turn out not to represent the implicand at all. Besides, even when the implicand is in there, the rule is harder to filter due to the other arguments which are not the implicand (@williampma correct me if I'm wrong).

We need to set an additional constraint on the rule format to make the implicand explicit. I think ideally we'd use a SetTVLink, see below.

Let's assume SetTVLink has the following format

SetTVLink
   <Atom>
   <TV>

So this would assign to . It's not clear what should be, it could be a TVLink that takes 2 NumberNode arguments, or something like that, anyway.

The rule would have the following format

BindLink
   <Variables> (optional)
   <Implicants>
   SetTVLink
      <Implicand>
      <TV>

For instance a deduction rule would look like

BindLink
   AndLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$B"
      ImplicationLink
         VariableNode "$B"
         VariableNode "$C"
   SetTVLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$C"
      ExecutionOutputLink
         GroundedSchemaNode "scm:deduction-formula"
         ListLink
            ImplicationLink
               VariableNode "$A"
               VariableNode "$B"
            ImplicationLink
               VariableNode "$B"
               VariableNode "$C"

the scheme code deduction-formula would still need to take Implication(A B) and Implication(B C) to get their TVs and compute the TV of Implication(A C).

If we don't want to wait for SetTVLink, we could still use that format replacing SetTVLink by ExecutionOutputLink + some scheme code, like

BindLink
   AndLink
      ImplicationLink
         VariableNode "$A"
         VariableNode "$B"
      ImplicationLink
         VariableNode "$B"
         VariableNode "$C"
   ExecutionOutputLink
      GroundedSchemaNode "scm:set-tv"
      ListLink
         ImplicationLink
            VariableNode "$A"
            VariableNode "$C"
         ExecutionOutputLink
            GroundedSchemaNode "scm:deduction-formula"
            ListLink
               ImplicationLink
                  VariableNode "$A"
                  VariableNode "$B"
               ImplicationLink
                  VariableNode "$B"
                  VariableNode "$C"

Slightly more verbose but allows to move on without having to define SetTVLink. Although I think taking the time to implement Set/Get TV links would be a good thing.

Also in both cases we could define some scheme function to build the BindLink given the rule's implicants, implicand and formula code. Or maybe store it that way, and let the URE build the BindLink as appropriate.

williampma commented 9 years ago

This looks to be the same problem mentioned in https://github.com/opencog/opencog/issues/1441 and https://github.com/opencog/opencog/pull/1593

Note that explicitly defining the output (implicand) of a rule is not always possible. Some rules could generate an infinite possible output (bases on some outgoing set of an input link, for example). I recall @bgoertzel wrote a solution (requiring some special yet to be invented system I recall). I couldn't find it at the moment (is it on google group or wiki... can't remember...)

ngeiswei commented 9 years ago

Maybe we don't need to have a single rule that expressive (generate an infinite possible output). We can always generate multiple simple rules via some scheme code, right?

amebel commented 9 years ago

http://wiki.opencog.org/w/Deep_types

bgoertzel commented 9 years ago

Yeah. I thought the best way to solve this problem was to introduce the "deep type system" i.e. "haskell or haskell-ish type system" suggested by Nil previously.... If the rule output has a type associated with it, then backward chaining can be done based on the type

On Tue, Jun 30, 2015 at 11:15 PM, Amen Belayneh notifications@github.com wrote:

http://wiki.opencog.org/w/Deep_types

— Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-117223478.

Ben Goertzel, PhD http://goertzel.org

"The reasonable man adapts himself to the world: the unreasonable one persists in trying to adapt the world to himself. Therefore all progress depends on the unreasonable man." -- George Bernard Shaw

ngeiswei commented 9 years ago

Deep type alone cannot fix the problem, we still need a way to tell "this is the implicand", and currently, as far as I can tell we don't have one, do we? Or is there already a convention regarding the arguments of the ExecutionOutputLink, like the first arg is the implicand (as suggested by @misgeatgit I believe)?

bgoertzel commented 9 years ago

Hmmm... I think there may be a couple problems mixed up here...

1) Is one problem that you removed the ImplicationLink from inside the BindLink??

Of course, a PLN rule needs an ImplicationLink --- it is, logically, an implication!!!

A rule needs to be of the form

ImplicationLink Premises Function for generating conclusions

Not all BindLinks need to involve ImplicationLinks, but PLN rules do

2) I see, you may be right that deep type alone is not enough..... Knowing the type of a conclusion, doesn't necessarily tell you enough to infer if some other rule is able to take that conclusion as a premise.

I wonder if we could express a rule something like

ImplicationLink Premises Output of function for generating conclusions

(optional) XXXLink (see below) Output of function for generating conclusions Template describing nature of output

...

The "template" would be an Atom-structure suitable for matching/chaining.

For instance, the rule Evaluation2Member(*,k)

described at

http://wiki.opencog.org/w/Deep_types

would look like

ForAllLink $D, $L, $k Implication Evaluation $D $L Member [123] ExecutionOutputLInk GSN “ElementAt” ListLink ListLink $L NumberNode $k SatisfyingSet Variable $V ExecutionOutputLink GSN “Insert” ListLink ListLink $L Variable $V NumberNode $k

ThereExists $X, $Y [456] EquivalenceLink [123] Member ConceptNode $X ConceptNode $Y

EvaluationLink PredicateNode "OutputTemplate" [123] [456]

...

The output template would then be used for chaining, and the actual output generation function [123] produces the specific output fitting into the template...

-- Ben

On Wed, Jul 1, 2015 at 4:26 AM, ngeiswei notifications@github.com wrote:

Deep type alone cannot fix the problem, we still need a way to tell "this is the implicand", and currently, as far as I can tell we don't have one, do we? Or is there already a convention regarding the arguments of the ExecutionOutputLink, like the first arg is the implicand (as suggested by @misgeatgit https://github.com/misgeatgit I believe)?

— Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-117331019.

Ben Goertzel, PhD http://goertzel.org

"The reasonable man adapts himself to the world: the unreasonable one persists in trying to adapt the world to himself. Therefore all progress depends on the unreasonable man." -- George Bernard Shaw

ngeiswei commented 9 years ago

@bgoertzel Adding the ImplicationLink back in the BindLink wouldn't add any new information, would it? Regardless of whether removing the ImplicationLink from BindLink was a bad idea, it seems independent of that problem.

Maybe I haven't been clear enough, the problem is that currently the formula, which is a black box, doesn't just take care of the TV but also of the whole output, so there is no way, unless the black box is run to get the output pattern. Your example about deep type is a good one, but completely ignores that issue, and the deep type does not reflect the shallow type (the syntactic hypergraph structure) we also want. I guess we want both shallow and deep type checkers that can run over the scheme code black box, it seems difficult to implement (we'd have to fiddle with scheme semantics), but it would indeed be the answer. Surely Shallow + Deep types contain all the information we need to perform the pattern matching on the target so select the rule! Or at least it's good enough (not getting into dependent types).

Now till we get good shallow and deep type checkers we still want to be able to run the backward chainer, there is definitely a lot of development to be done on it and I don't think we should postpone URE development till we get good type checkers.

So meanwhile what I suggest is to come up with a convention to get that output structure. The SetTVLink is a clean way to split that black box into a clear box part and a black box part containing only the formula, and therefore let the output structure visible. There are other ways. In the absence of other suggestions I'll probably settle with @misgeatgit 's, like the first argument of the formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start working on the type system.

bgoertzel commented 9 years ago

On Wed, Jul 1, 2015 at 3:57 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel Adding the ImplicationLink back in the BindLink wouldn't add any new information, would it?

Using an ImplicationLin here would just make the Atomspace formulation of PLN rules semantically correct...

An inference rule IS an implication: premises IMPLY conclusions, and the current Atomspace formulation does not reflect this...

I don't think ImplicationLInks are ALWAYS needed with BindLinks, but in this case, we really really do have a probabilistic-logical Implication, no?

Maybe I haven't been clear enough, the problem is that currently the formula, which is a black box, doesn't just take care of the TV but also of the whole output, so there is no way, unless the black box is run to get the output pattern. Your example about deep type is a good one, but completely ignores that issue, and the deep type does not reflect the shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS the "syntactic hypergraph structure", isn't it?

Now till we get good shallow and deep type checkers we still want to be

able to run the backward chainer, there is definitely a lot of development to be done on it and I don't think we should postpone URE development till we get good type checkers.

Agreed

So meanwhile what I suggest is to come up with a convention to get that output structure. The SetTVLink is a clean way to split that black box into a clear box part and a black box part containing only the formula, and therefore let the output structure visible. There are other ways. In the absence of other suggestions I'll probably settle with @misgeatgit https://github.com/misgeatgit 's, like the first argument of the formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start working on the type system.

Agree on both points...

ben

ngeiswei commented 9 years ago

On 07/01/2015 11:04 AM, bgoertzel wrote:

On Wed, Jul 1, 2015 at 3:57 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel Adding the ImplicationLink back in the BindLink wouldn't add any new information, would it?

Using an ImplicationLin here would just make the Atomspace formulation of PLN rules semantically correct...

An inference rule IS an implication: premises IMPLY conclusions, and the current Atomspace formulation does not reflect this...

I don't think ImplicationLInks are ALWAYS needed with BindLinks, but in this case, we really really do have a probabilistic-logical Implication, no?

Well, the ImplicationLink can definitely have a valid PLN interpretation (although the TV on the ImplicationLink, or its quantifier, would need to be properly computed), and surely this would be a valuable knowledge for OpenCog to reason about its own reasoning process. Other than that I don't think it is needed, it certainly isn't for the URE to work properly. The day we need to have OpenCog to reason about its own reasoning process, we can build those ImplicationLinks.

Maybe I haven't been clear enough, the problem is that currently the formula, which is a black box, doesn't just take care of the TV but also of the whole output, so there is no way, unless the black box is run to get the output pattern. Your example about deep type is a good one, but completely ignores that issue, and the deep type does not reflect the shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS the "syntactic hypergraph structure", isn't it?

Sure, it is. I mean that in case the output template is hidden, a shallow type engine could infer it back, that could be cool.

Nil

Now till we get good shallow and deep type checkers we still want to be

able to run the backward chainer, there is definitely a lot of development to be done on it and I don't think we should postpone URE development till we get good type checkers.

Agreed

So meanwhile what I suggest is to come up with a convention to get that output structure. The SetTVLink is a clean way to split that black box into a clear box part and a black box part containing only the formula, and therefore let the output structure visible. There are other ways. In the absence of other suggestions I'll probably settle with @misgeatgit https://github.com/misgeatgit 's, like the first argument of the formula black box must be the output.

I suggest that as soon as the URE is working "well enough", we can start working on the type system.

Agree on both points...

ben

— Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-117517878.

bgoertzel commented 9 years ago

Well, the ImplicationLink can definitely have a valid PLN interpretation (although the TV on the ImplicationLink, or its quantifier, would need to be properly computed), and surely this would be a valuable knowledge for OpenCog to reason about its own reasoning process. Other than that I don't think it is needed, it certainly isn't for the URE to work properly. The day we need to have OpenCog to reason about its own reasoning process, we can build those ImplicationLinks.

I dunno... having the rules represented in such a semantically opaque format just seems wrong to me.... I understand it won't stop the URE from working but eventually it will bite us in the ass somehow...

I guess I'll have to think more about whether this reformulation of the rules is merely inelegant and morally offensive ;), or actually going to be problematic in the mid-term future... Hmm...

Anyway, I agree this is not the most urgent problem. Getting the chainer working is certainly more important. But after that, I personally would like to see the rules represented in a semantically transparent way...

Maybe I haven't been clear enough, the problem is that currently the formula, which is a black box, doesn't just take care of the TV but also of the whole output, so there is no way, unless the black box is run to get the output pattern. Your example about deep type is a good one, but completely ignores that issue, and the deep type does not reflect the shallow type (the syntactic hypergraph structure) we also want.

Yes, but my "OutputTemplate" does address this -- the output template IS the "syntactic hypergraph structure", isn't it?

Sure, it is. I mean that in case the output template is hidden, a shallow type engine could infer it back, that could be cool.

True. But it might be inefficient for the type engine to have to infer it each time, right? So the OutputTemplate would be a cache...

ben

amebel commented 9 years ago

@ngeiswei

how will the new schema for rules solve the black-box issue for Evaluation2Member rule, let say with a predicate having 2 or 3 arguments?
What is the semantics of SetTVLink?

ngeiswei commented 9 years ago

On 07/01/2015 12:29 PM, Amen Belayneh wrote:

@ngeiswei https://github.com/ngeiswei

how will the new schema for rules solve the black-box issue for Evaluation2Member rule, let say with a predicate having 2 or 3 arguments?

It doesn't. You'd still need to split that complex rule into multiple simpler ones. I think it's OK because ultimately you don't need a very large number of them, say 3 or 4, maybe up to 10 in a distant future. And one can easily write some scheme code that would generate them all up to a certain N.

So if it doesn't solve that, what does it solve? It replaces the current code that assumes any argument of the ExecutionOutputLink can be the output by something else so that only one output, the correct one, is assumed.

What is the semantics of SetTVLink?

SetTVLink Atom TV

assigns truth value TV to atom Atom and returns Atom.

This would be cool, I might implement it, but we can also assume that the first argument of the implicand ExecutionOutputLink is the output. The other option is to replace SetTVLink by ExecutionOutputLink "scm: cog-set-tv!", it's cooler but more verbose.

BTW, IMO the main semantical opacity comes from the black box scheme code, SetTVLink is a step towards turning this black box into a clear box.

Hmm, SetTVLink should be pretty easy to implement, maybe I'll do that tomorrow.

Or alternatively a rule would be defined as a triplet

(Implicant, Implicand, TV formula)

Maybe that would be better, it's very terse and can be turned into whatever you need. Or a scheme function that given this triplet (as say 3 scheme arguments), turn that into a rule.

So 5 options:

Use 1st arg of the implicand's ExecutionOutputLink as output
Use SetTVLink
Use another ExecutionOutputLink + cog-set-tv!
Use a triplet (Implicant, Implicand, TV formula)
Use scheme code to generate rules given that triplet

If I were the only one working on OpenCog I would probably go with 5 (for the user), then go with 3 (for the algorithm).

Let me know what you think. Ultimately multiple choices are possible. We could support 1 in the case of black box for the existing rules. And support 3 and 5 for new rules.

However I would definitely not stay in the current situation where any argument is assumed to be output.

Or I can implement SetTVLink and convert all existing rules to follow that format, which would be both clean and terse.

— Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-117560928.

williampma commented 9 years ago

Thinking ahead, which solution (1-5) will work best when the DeepType system is eventually implemented (so that when that is implemented, the effort here won't be wasted)?

ngeiswei commented 9 years ago

But the deep type system isn't gonna fix all the issues, it's not gonna reveal an output structure hidden in a scheme function. I think the best solution is to use 2+5, but meanwhile 3+5 prevents from implementing a SetTVLink. I'll see how the existing rules can fit into 1, if they easily can maybe I'll go that way.

williampma commented 9 years ago

True, but it is still part of "showing the true rule's output" solution. I am just wondering if any of the solution will became incompatible with the deep type's solution (ie. when deep type's development begin, the developer might end up removing the solution here to get a good representation working for deep type). A representation is needed so both system can coexist I think?

ngeiswei commented 9 years ago

Having powerful shallow + deep type systems maybe remove the need for expliciting the output structure, but it certainly wouldn't be in contradiction with using a more transparent description, with SetTVLink for instance.

Anyway, I do understand your concern about investing too much energy into an temporary solution. I'm about to go through all existing rules to see if solution 1 can easily be used, if that is the case we go that way, end of the debate. If that isn't the case, we must think...

ngeiswei commented 9 years ago

OK, so here's my report, only looking at PLN rules (I tried to look at relex2logic but the comments were too obscure for me to understand the rules)

Rules with output pattern as first argument

abduction.scm context-free-to-sensitive.scm contextualize.scm decontextualize.scm equivalence-transformation-rule.scm evaluation-to-member.scm inheritance-to-member.scm member-to-inheritance.scm modus-ponens.scm

Rules with output pattern as last argument

and-breakdown-rule.scm and-simplification-rule.scm and-to-context.scm and-transformation-rule.scm deduction.scm not-elimination-rule.scm not-simplification-rule.scm or-breakdown-rule.scm or-simplification-rule.scm or-transformation-rule.scm

Rules with no output pattern (hidden in the scheme code)

and.scm member-to-evaluation.scm not.scm or.scm

Rules with multiple outputs

and-elimination-rule.scm or-elimination-rule.scm

I thinking, there might be another way, more soon...

ngeiswei commented 9 years ago

OK, so the problem, and I had not realized that before looking at all these rules, some rules have multiple outputs, I don't know if that's a good idea, but if we really wish to support that, here's my suggestion:

Suggestion

Run the scheme code over the (ungrounded) patterns to unravel the output structure!

ngeiswei commented 9 years ago

That way we don't care were the output is, or even if there's one. I think it would work, but we'd need to try to know for sure...

ngeiswei commented 9 years ago

Thinking about it, it is a hacky way to infer the output's shallow type. So once we have a shallow type (and ultimately a deep type) system we can drop this hack (if it's gonna work anyway).

williampma commented 9 years ago

Run the scheme code over the (ungrounded) patterns to unravel the output structure!

Only possible if the scheme code is simple. If the rule matched a variable to a link and the scheme code looks inside the link, then the ungrounded pattern will not have the information.

But may not be a problem for the PLN rules you listed. Just not in general.

williampma commented 9 years ago

Would it be better to merge @prateeksaxena2809's changes before changing the rule's format?

ngeiswei commented 9 years ago

I won't change the rule format, I'll first try the run-scheme-formula hack.

But sure, create a pull request and let's merge it.

amebel commented 9 years ago

I am not sure on which issue that @ngeiswei suggested it, but wouldn't the introduction of regex + and * link and making a modification to the rule definition schema as follows solve black-box rules, for the backward chainer?

(EvaluationLink
     (PredicateNode "output_structure")
     (ListLink
        (ConceptNode "PLN-Evaluation2Member")
        (SignatureLink
            (TypeNode "MemberLink")
            (RegexPlusLink ; this acts on node type, and may inherit from singaturelink
                (TypeNode "VariableNode")
            )
            (SignatureLink
                (TypeNode "SatisfyingSetLink")
                (TypeNode "VariableNode")
                (SignatureLink
                    (TypeNode "EvaluationLink")
                    (TypeNode "PredicateNode")
                    (SignatureLink
                        (TypeNode "ListLink")
                        (RegexStarLink
                            (TypeNode "ConceptNode")
                        )
                        (RegexStarLink
                            (TypeNode "VariableNode")
                        )
                        (RegexStarLink
                            (TypeNode "ConceptNode")
                        )
                    )
                )
            )
        )
    )
)

I am not that privy of regex. Reference http://wiki.opencog.org/w/SignatureLink

ngeiswei commented 9 years ago

@AmeBel thanks for your input. I actually wasn't aware the pattern matcher's type checker was that advanced (I do understand your regex notation are not implemented, I'm basing that on reading the SignatureLink wiki page).

So yes, a solution could be to specify the shallow type of the output elsewhere, in addition to the rule definition, and have the backward chainer relies on that. That way it wouldn't change the rule format. It would add an extra burden on the user to declare the type though. In order not to add any extra burden to the user the type checker must be able to infer the type's output, I don't think that's currently possible. But anyway, I'm first gonna see if the hack I've lastly suggest would work, if it does, I'll move on to the next issue.

linas commented 8 years ago

is this still an issue?

ngeiswei commented 8 years ago

This still an issue.

bgoertzel commented 8 years ago

You implemented your “hack”? On 7 Apr 2016 4:04 pm, "ngeiswei" notifications@github.com wrote:

Closed #119 https://github.com/opencog/atomspace/issues/119.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#event-617986484

ngeiswei commented 8 years ago

It is no longer a hack :-)

Of course the BC itself still requires a major rewrite.

ngeiswei commented 8 years ago

Oh, to answer the question, no I didn't implement the hack consisting to run the GSN with the variables. After exploring a few rules I realized this wouldn't work as William rightly warned. Instead the user has the possibility to specify a number of output patterns.

bgoertzel commented 8 years ago

Hmm. Can you explain more explicitly, maybe with some good example? On 7 Apr 2016 4:19 pm, "ngeiswei" notifications@github.com wrote:

Oh, to answer the question, no I didn't implement the hack consisting to run the GSN with the variables. After exploring a few rules I realized this wouldn't work as William rightly warned. Instead the user has the possibility to specify the number of output patterns.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-206755583

ngeiswei commented 8 years ago

@bgoertzel I've improved the wiki http://wiki.opencog.org/wikihome/index.php/URE_Configuration_Format#Rule_Definition and added links to examples using only the forward form and both forward and backward forms. Let me know if it's not clear enough.

Of course ultimately with a kick ass deep type checker (such as what we might get by borrowing from Agda's) the backward forms wouldn't be necessary. However till then it is necessary in order to move the BC code forward.

bgoertzel commented 8 years ago

Got it, that's very clear now, thanks ;)

On Thu, Apr 7, 2016 at 7:08 PM, ngeiswei notifications@github.com wrote:

@bgoertzel https://github.com/bgoertzel I've improved the wiki http://wiki.opencog.org/wikihome/index.php/URE_Configuration_Format#Rule_Definition and added links to examples using only the forward form and both forward and backward forms. Let me know if it's not clear enough.

Of course ultimately with a kick ass deep type checker (such what we might get by borrowing from Agda's) the backward forms wouldn't be necessary. However till then it is necessary in order to move the BC code forward.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-206819732

Ben Goertzel, PhD http://goertzel.org

"I am Ubik. Before the universe was, I am. I made the suns. I made the worlds. I created the lives and the places they inhabit; I move them here, I put them there. They go as I say, then do as I tell them. I am the word and my name is never spoken, the name which no one knows. I am called Ubik, but that is not my name. I am. I shall always be.” -- Ubik

linas commented 8 years ago

There's a fair amount of infrastructure for specifying types. Its mostly unused. it will remain mostly under-developed as long as no one uses it. From what I can tell, the one thing that agda has that atomese doesn't is dependent types. Well, that and I suppose lots of assorted infrastructure; type inference support is weak or unusable depending on what you want to do. I'm convinced that the pattern matcher can do arbitrarily complex type inference. One just has to start experimenting.

The DualLink can be used to search not only for premises, but also for consequents, so could be used to identify backwards-direction rule candidates. The initial implementation doesn't do type checking; I thought about that, and punted, since I figued no one wanted that or used that; but it can be added, and should not be hard.

I'm pretty sure we've got most of the right infrastructure for this kind of stuff, although there are bugs and rough edges and assorted missing bits and pieces.

bgoertzel commented 8 years ago

Interesting. Let us remember to discuss this in depth when you and Nil are in HK in May...

On Sat, Apr 16, 2016 at 6:42 AM, Linas Vepštas notifications@github.com wrote:

There's a fair amount of infrastructure for specifying types. Its mostly unused. it will remain mostly under-developed as long as no one uses it. From what I can tell, the one thing that agda has that atomese doesn't is dependent types. Well, that and I suppose lots of assorted infrastructure; type inference support is weak or unusable depending on what you want to do. I'm convinced that the pattern matcher can do arbitrarily complex type inference. One just has to start experimenting.

The DualLink can be used to search not only for premises, but also for consequents, so could be used to identify backwards-direction rule candidates. The initial implementation doesn't do type checking; I thought about that, and punted, since I figued no one wanted that or used that; but it can be added, and should not be hard.

I'm pretty sure we've got most of the right infrastructure for this kind of stuff, although there are bugs and rough edges and assorted missing bits and pieces.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/opencog/atomspace/issues/119#issuecomment-210672481

Ben Goertzel, PhD http://goertzel.org

"I am Ubik. Before the universe was, I am. I made the suns. I made the worlds. I created the lives and the places they inhabit; I move them here, I put them there. They go as I say, then do as I tell them. I am the word and my name is never spoken, the name which no one knows. I am called Ubik, but that is not my name. I am. I shall always be.” -- Ubik

opencog / atomspace

Make rule implicand explicit for the backward chainer #119

Rules with output pattern as first argument

Rules with output pattern as last argument

Rules with no output pattern (hidden in the scheme code)

Rules with multiple outputs

Suggestion