Hi Linas, thanks for the response :) I'll try to explain myself and provide a link to a project supporting my reasoning. If I'm not mistaken, you are talking about *link grammar* rules capable of doing inference process. The similar thing I'm trying to articulate is an extension to more popular grammar production rules which renders them deductively complete. The result stands for URE equivalent capable of reasoning about flexible syntax expressions (may be non-strict syntax form of Atomspace). Basically, it is a fusion between term rewriting rules and classical logic.
Usual parsers take productions of the form `A -> B` (I write this backwards to align it with logic, as explained in correspondence between production rules and logical implication <https://github.com/contrast-zone/exp-log/blob/master/docs/introduction.md#321-correspondence-between-production-rules-and-logical-implication> section). Within the extension I propose, having a kind of a production: *A1 /\ A2 -> B* reads as follows - when checking for `B`, we derive *both* `A1` *and* `A2` to be parsed in the same input string fragment at the appropriate place. Similarly, *A -> B1 \/ B2* means that if *either* `B1` *or* `B2` is priorly derived, then derive `A` to parse in input string fragment at appropriate place. This extension to the parsing is a matter of expecting ambiguous expressions, and it comes handy when parsing logical expressions during proof construction. I imagined the whole inference mechanism around these extensions. I named it "expression logic" <https://github.com/contrast-zone/exp-log/blob/master/docs/introduction.md>, and it represents all of the following: expression recognizer and generator, SMT solver, deductive system, term rewriting framework, and metatheory language formalization. In less words, it is a problem solver. Implementation is still a work in process, but I believe that background theory won't change too much. I'm trying to keep the size of the whole implementation below 300 javascript LOC. Putting once more the background theory on trial, I wonder if the planned logic operators can be described only using basic term rewriting rules (only rules of the form `A -> B`) while retaining deductive completeness. Supported logic operators would still have the same significance to the theory behind, only that they would be implemented as a library, a level above the bare metal term rewriting algorithm. I hope I managed to be more understandable this time. Thanks again for the response, - ivan - pet, 2. tra 2021. u 19:09 Linas Vepstas <[email protected]> napisao je: > Hi Ivan, > > On Fri, Apr 2, 2021 at 3:00 AM Ivan V. <[email protected]> wrote: > >> >> >> I'm approaching a similar problem from the similar side. I start with a >> parsing algorithm, and extend it to support left side conjunctions and >> right side disjunctions. >> > > I don't understand what you are saying here. What does it mean to extend a > parser in this way? What do you mean by conjunctions and disjunctions? > > The conventional definition of a parser is a device that acts on a string > of symbols, that, when it's done, indicates how that string can be > decomposed into parts. > > The conventional definition of conjuncts and disjuncts are strings of > symbols combined with and/or operators. > > How are you modifying these conventional definitions to obtain what you > are doing? > > -- Linas > > This extension makes the rules equivalent to normalized sequents known >> from sequent calculus. The result is very interesting: any logical formula >> can be converted to these normalized sequents suitable for (enhanced) >> parsing. All rules then become: >> >> A1 /\ A2 /\ A3 /\ ... -> B1 \/ B2 \/ B3 \/ ... >> >> The parsing process then becomes equivalent to the logical abduction >> process. We start from the `Goal` atom and chain rules backwards to >> verify if the input string matches the rules. >> >> I like to think that this system resembles a kind of URE on steroids. >> >> >> pet, 2. tra 2021. u 04:27 Linas Vepstas <[email protected]> napisao >> je: >> >>> Not everyone is aware that Link Grammar's underlying theory is far more >>> broad than simply describing natural language. It would seem that the >>> theory generalizes to one of describing graphs, in general (and knowledge >>> graphs, in particular). >>> >>> I just updated the wiki page https://wiki.opencog.org/w/Link_Grammar to >>> give a brief sketch of how this theory generalizes, and how it influences >>> the AtomSpace design. The generalization is reviewed in >>> https://wiki.opencog.org/w/Connectors_and_Sections >>> >>> If you've heard these ideas before, then this page "doesn't say anything >>> new"; it just reminds you of the names of the Atoms that implement the >>> various concepts, such as connectors and disjuncts (connector sequences). >>> It also points to the half-dozen PDF's that justify and articulate this >>> generalization. >>> >>> If you haven't heard of these ideas before... well, enjoy! Just be aware >>> that the ideas are deceptively simple. You might read this stuff and nod to >>> yourself "yes, of course, obvious" until you get to something like the >>> https://wiki.opencog.org/w/CrossSection and wonder "what the heck?" The >>> apparent simplicity of these concepts makes them sometimes hard to >>> understand. >>> >>> -- Linas >>> >>> -- >>> You received this message because you are subscribed to the Google >>> Groups "opencog" group. >>> To unsubscribe from this group and stop receiving emails from it, send >>> an email to [email protected]. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/opencog/CAHrUA378PEv7%3Dm4A2yte-1icmL32JYrd-EndgE%2BuHGZvzAgc%3Dg%40mail.gmail.com >>> <https://groups.google.com/d/msgid/opencog/CAHrUA378PEv7%3Dm4A2yte-1icmL32JYrd-EndgE%2BuHGZvzAgc%3Dg%40mail.gmail.com?utm_medium=email&utm_source=footer> >>> . >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "opencog" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/opencog/CAB5%3Dj6W5VnC-2A_k%3D3Vc2rV29%3DKuKLhddQzBXgpXsxc%3Dm%2BbuWw%40mail.gmail.com >> <https://groups.google.com/d/msgid/opencog/CAB5%3Dj6W5VnC-2A_k%3D3Vc2rV29%3DKuKLhddQzBXgpXsxc%3Dm%2BbuWw%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > > > -- > Patrick: Are they laughing at us? > Sponge Bob: No, Patrick, they are laughing next to us. > > > -- > You received this message because you are subscribed to the Google Groups > "opencog" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/opencog/CAHrUA36Sm5O_SYqYJ-WxqLSNcq%3DD6aoRm8rZ4UPVVFU2Nq%3DqGg%40mail.gmail.com > <https://groups.google.com/d/msgid/opencog/CAHrUA36Sm5O_SYqYJ-WxqLSNcq%3DD6aoRm8rZ4UPVVFU2Nq%3DqGg%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "opencog" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAB5%3Dj6VTy259EpZ55CqeH8u7QhM3x8U3DXOG7VEQf2uymBCyVg%40mail.gmail.com.
