I think this was ye olde original paper on parsing as deduction, http://aclweb.org/anthology/P89-1033
There's a whole literature on theorem-proving for categorial grammars of course https://arxiv.org/abs/cmp-lg/9508009 So there's a lot of ways to show that parsing is a kind of deductive inference The other way around, that "deductive inference is a kind of parsing", seems to require a bit of a stretch of the concept of "parsing" ... On Fri, Dec 14, 2018 at 1:48 PM Zar Goertzel <[email protected]> wrote: > > Howdy Linas, > > Unfortunately, I'm drastically ignorant compared to my senior colleagues and > you. > > Re: URE: So curry-howard says "proofs are programs" and it turns out > that theorem proving is a lot like parsing (its identical to > parsing???) I DO NOT know of any simple write-up of this topic; I can > only wave my hands around. When I mentioned this to Ben's son Zar, he > kind-of responded and said "duhh its obvious everyone knows this." > > Zar, do you know of any nice readable references that explain how > theorem-proving and parsing are "the same thing"? > > > We had happened to be talking about it at lunch when you brought that up. It > seems likely they're in a similar state to you: it seems obvious and they can > wave their hands around, but haven't bothered formally writing it up. > > Would it be hard to write up formally? > > On Wed, Dec 12, 2018 at 1:17 AM Linas Vepstas <[email protected]> wrote: >> >> Oh, and one more (minor?) remark: the intermediate states that get >> explored during pattern matching are called "Kripke frames", and the >> "crisp logic of term re-writing" is one of the modal logics. I know >> this to be true in a hand-waving fashion; I have searched long and >> hard for a paper or a book that would articulate this in some direct, >> detailed fashion. I have not yet found one. >> >> Zar, so second question, any chance at all you might be aware of >> references for this? > > > The logic of term rewriting is paramodulation? That's not a modal logic > though . . . > >> >> >> --linas >> On Tue, Dec 11, 2018 at 2:24 AM Ivan Vodišek <[email protected]> wrote: >> > >> > Linas, >> > >> > Thank you for taking a time to response, I'll try to keep this short. I >> > might be wrong, but Curry-Howard-Lambek isomorphism inspires me greatly in >> > a pursuit for one-declarative-language-like-URE-to-rule-them-all. >> > >> > I see term rewriting simply as basic implication over input and output >> > terms. A number of term rewriting rules may be bundled together in a >> > conjunction. Alternate pattern-matching options may form a disjunction. >> > And pattern exclusion may be expressed as a negation. These are all common >> > logical operators in a role of defining a term rewriting system. And since >> > this kind of term rewriting is basically a logic, it can generally be >> > tested for contradiction, or it can be used for deriving relative indirect >> > rules - if we want it so. >> > >> > That's a short version of what I currently work on - a term rewriting >> > system expressed as a crisp logic - just a few basic logic operators with >> > no hard-wired constants other than true and false - all wrapped up in a >> > human friendly code code processor. >> > >> > - Ivan V. - >> > >> > uto, 11. pro 2018. u 04:07 Linas Vepstas <[email protected]> napisao >> > je: >> >> >> >> On Sun, Dec 9, 2018 at 11:55 AM Ivan Vodišek <[email protected]> wrote: >> >> > >> >> > Oh, I see, I must be talking about URE then. All cool, then it seems >> >> > reasonable to me (one ring to rule them all - policy). >> >> > >> >> > I keep persuading myself that a perfect single declarative - logic + >> >> > lambda calculus + type theory exists, or could be invented, >> >> >> >> So, OK, the atomspace is trying to be: >> >> >> >> + declarative: so kind-of-like datalog or kind-of like SQL or noSQL, >> >> or some quasi-generic (graph) data store. But you already know this. >> >> >> >> - it does NOT have "logic" in it, in any traditional sense of the word >> >> "logic". It does have the ability to perform term-rewriting (pattern >> >> re-writing, graph re-writing). >> >> >> >> - lambda calculus is a form of "string rewriting". Note that string >> >> rewriting is closely related to term rewriting (but not quite the same >> >> thing) and that term rewriting is closely related to graph rewriting >> >> (but not quite the same thing). >> >> >> >> When lambda calculus was invented, any distinction between strings, >> >> terms, and graphs was unknown and unknowable, until the basic concepts >> >> got worked out. So, due to "historical accident", generic lambda >> >> calculus remains a string rewriting system. As stuff got worked out >> >> over the 20th century, the concept of "term rewriting" gelled as a >> >> distinct concept. (And other mind-bendingly >> >> similar-but-slightly-different ideas, like universal algebra, model >> >> theory ... and bite my tongue. There's more that's "almost the same as >> >> lambda calc. but not quite". A veritable ocean of closely related >> >> ideas.) >> >> >> >> From practical experience with atomspace, it turns out that trying to >> >> pretend that all three rewriting styles (string, term, graph) are the >> >> same thing "mostly works", but causes all kinds of friction, >> >> confusion, conundrums in detailed little corners. So, for example, >> >> BindLink was an early attempt to define a Lambda for declarative >> >> graphs. In many/most ways, it really is "just plain-old-lambda". It >> >> works, and works great to this day, but, never-the-less, we also >> >> created more stuff that is "just like lambda, but different", >> >> including LambdaLink, etc. >> >> >> >> In many ways, its an ongoing experiment. The search for "perfect" has >> >> more recently lead to "values", which are a lot like "valuations" in >> >> model theory. (and again, recall that model-theory is kind-of-ish like >> >> lambda-calculus, but its typed.) >> >> >> >> There's no "logic" in the atomspace, but you could add logic by using >> >> the URE, and/or by several other ways, including parsing, sheaves, and >> >> openpsi. In short, there's lots of different kinds of logic, and lots >> >> of different ways of implementing it, and we are weakly fiddling with >> >> several different approaches. And I have more in mind, but lacking in >> >> time. >> >> >> >> -- Linas >> >> -- >> >> cassette tapes - analog TV - film cameras - you >> >> >> >> -- >> >> 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 post to this group, send email to [email protected]. >> >> Visit this group at https://groups.google.com/group/opencog. >> >> To view this discussion on the web visit >> >> https://groups.google.com/d/msgid/opencog/CAHrUA35V2Uk0YbwERPMkPhpxevriT0DZvaYzLtEPXUQC9TiUHQ%40mail.gmail.com. >> >> For more options, visit https://groups.google.com/d/optout. >> > >> > -- >> > 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 post to this group, send email to [email protected]. >> > Visit this group at https://groups.google.com/group/opencog. >> > To view this discussion on the web visit >> > https://groups.google.com/d/msgid/opencog/CAB5%3Dj6VaDej%3DGBL3bpMxYArP6ZnkifCiNmStc7-SrJO%2BV3eHQA%40mail.gmail.com. >> > For more options, visit https://groups.google.com/d/optout. >> >> >> >> -- >> cassette tapes - analog TV - film cameras - you > > -- > 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 post to this group, send email to [email protected]. > Visit this group at https://groups.google.com/group/opencog. > To view this discussion on the web visit > https://groups.google.com/d/msgid/opencog/CAHY-%3DHGbf_Cc%2BsaQ%3DFiEw0bwB8G_607vVNMNY6-Jb3zFYyVf3Q%40mail.gmail.com. > For more options, visit https://groups.google.com/d/optout. -- Ben Goertzel, PhD http://goertzel.org "The dewdrop world / Is the dewdrop world / And yet, and yet …" -- Kobayashi Issa -- 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 post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/opencog. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CACYTDBfw%3D5x7Pu0%3DW6tt2hRgPpQBrmxDK_8TjxsB2HMGvoBJLg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
