Hi Alex, Let me top-post reply to your email; it will be simpler that way.
The part of opencog you are interested in is called "the atomspace" -- it already is a graph database; it is implemented in C++, and scheme is one of the languages that have an API to it. (there is also python and haskell, and of course native C++ as well). Its a "graph database" in the sense that you can save and restore to disk (currently via postgresql, but an internal API allows others) It is a "graph database" in that it has a query language, called "pattern matching": you can create arbitrarily complex queries, and it will return only those graphs that match your query. Do not confuse this "pattern matching" with that in other programming languages: it is MUCH MUCH more powerful and flexible. Its a real query language. and it can query more than just relations, it can also query terms. The atomspace implements a data representation language called "atomese". There are two parts to it: the atoms, and the values. An atom is kind-of-like an "atomic sentence" or a "term", I'm not sure what they call in the proof assistance, but in model theory and in proof theory, there is a general concept of an atomic term, and that's what opencog atoms are. The atomese "values" are what the mathematicians call "valuations", and are closely related to "interpretations" -- again, I suspect these are the words that the proof assistants use, and the atomese values correspond to those. The big difference is that the atemese values do not have to be just true or false, but can be any floating point number, or any array of numbers, or any array of strings, or any tree of numbers and strings. They still should be though of as being like "valuations" or "interpretations". They also can be saved and stored to disk, i.e. they are a part of the database. They cannot be queried -- that is how they differ from atoms. They are faster, smaller, lighter. Oh, I should mention that atomese includes a type system with a fairly rich collection of type constructors, including some of the whizzier ones that the proof assistants like to talk about. Yes, atomese is self-modifying. The pattern matcher is in fact a kind-of term-rewriter, and so the atomspace comes with a term-rewriting engine, built in. OpenCog has always wanted to have some kind proof assistant or some kind of reasoning engine layers on top of the atomspace. We've made some strides in that direction: the "universal rule engine" -- URE -- but it still does not use some of the more famous algorithms for applying rules and keeping track of valuations. The URE is intended to allow different kinds of reasoning to be layered on top of it, PLN being the primary one, but others are possible. I have long wanted to attach an ASP (answer-set programming) engine to the atomspace. In the same vein,attaching a proof assistant would also be good. Either attachment would probably by-pass the URE and the pattern matcher, and directly manipulate the atoms and the valuations. --linas On Wed, Sep 20, 2017 at 1:23 AM, Alex <[email protected]> wrote: > I am back to OpenCog from my travels to the land of proof assistants > (mainly Coq and Isabelle/HOL, I decided to stick with Coq as it is far more > better documented and lambda-Pi-omega calculus is the most extensive > formalism for which one can hope, besides there are pretty extensive > formalization efforts with applications). So - I can use proof assistants > for implementation of any more or less formal reasoning process. > > Now I am in great need for the knowledge repsesentation, knowledge base > and OpenCog is very universal and promising project. > > OpenCog uses Scheme as knowledge representation language (as I understand, > then this is one from many options for interfacing with OpenCog). So - this > is natural question - *how close are valid Scheme programms to the > sentences of OpenCog knowledge? Are OpenCog knowledge encoding sentences > the real Scheme programs or real fragments of the Scheme programs?* E.g. > maybe Node definition is Scheme variable/instance declaration, maybe link > definition is Scheme data structure declaration? > > There is homoiconicity in Scheme language - Scheme code is the data and > Scheme data is the code. So - one can represent the data/declarative or > procedural knowledge with the Scheme code. > > If OpenCog sentences are more or less valid Scheme programs and if Scheme > programs are data structures, then the following question arise - *how > can we represent Scheme programs as data structures - can current > production ready graph databases (Neo4j) be used for the storing the Scheme > programs and for the querying Scheme programs and also - for executing > Scheme programs?* If such represenation is possible then maybe it is > possible to move OpenCog knowledge bases (as Scheme programs) to graph > databases. I am suspicious about Neo4J, because it is commercial database, > but Apache ArangoDB can be very good options, because it is open source and > it known to be very scalable. I am a bit suspicous whether OpenCog > infrastructure can compete with the commercial ready databases. And if > Scheme programs can be represent in current database then we can keep > OpenCog philosophy, knowledge base code, agent code and gain the > scalability of graph databases... > > If OpenCog knowledge base (AtomSpace) is the big Scheme program then we > can consider also the self-modification of this program. And even more - > Scheme language as functional programming language is connected to lambda > calculus and lambda calculi are the prime formalism for the reasearch and > implementation of the Goedel machine. So - *self modifying OpenCog > atomspace (as Scheme program) can be the Goedel machine or at least the > seed of Goedel machine or the seed of AGI?* > > *So - are there thoughts and ideas floating around along the lines that I > have described?* > > -- > 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/1a6823b8-0479-4469-a2ac-47a36b1c2140%40googlegroups.com > <https://groups.google.com/d/msgid/opencog/1a6823b8-0479-4469-a2ac-47a36b1c2140%40googlegroups.com?utm_medium=email&utm_source=footer> > . > For more options, visit https://groups.google.com/d/optout. > -- *"The problem is not that artificial intelligence will get too smart and take over the world," computer scientist Pedro Domingos writes, "the problem is that it's too stupid and already has." * -- 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/CAHrUA34MEZipkmMQG5pTZMk5eb2twawNpA0DhsSSMPq0NWJ%2Big%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
