Well - here was mentioned idea that Atomspace/Atomese can be perceived like logical framework, like meta-logic in which every other kind of logic can be encoded. Well - logic is deductive reasoning and deductive reasoning is only one type of reasoning besides inductive, abductive and analogical reasoning. So - maybe not just meta-logic but even more - meta-reasoning system...
But I was taken aback by the fact, that PLN (and NARS) currently is based on Aristotelian term logic (just monadic fragment of the first order predicate logic), as I understand. I believe that PLN can be extended to full predicate logic or even to more general logics, but for my present endeavours I have decided to use Atomspace and Atomspace Scheme for the encoding of the entire knowledge base (facts, rules) but for the specific reasoning tasks I will try to call external reasoning system. For example, legal reasoning (of which I am fan) consists from the commonsense reasoning which can be done in Atomspace but also it consists - in special cases - from formal inference that should be done in specific logics (e.g. deontic defeasible logics). In this formal case I will formulate this subtask in the terms of Atomspace and I will try to forward this subtask to the external reasoning engine and this engine will do reasoning and it will give results to Atomspace and I will be able to continue my inference in Atomspace with some strongly and provably deduced facts. *How this sounds? Is it possible to call external functions from the Atomspace? E.g. can Atomspace BindLink call external program in its rule head?* For the external reasoning system I have choosen Coq proof asistant (which I am currently learning) which is capable of acting as meta-logic framework and in which it is possible to encode wealth of logics (e.g. http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ Working with linear logic in Coq). Well - there are lot of meta-logic systems - including MMT project (Latin) https://kwarc.info/people/frabe/Research/rabe_habil_14.pdf and also other proof assistants but there are so much good references about Coq that I am sticking to it. There is long way to go before Atomspace can be used as strong meta-logic framework - provable and formal syntax and semantics should be defined for the Atomspace parts (maybe subset of Atomese atom and link types) that will be used in formal/rigorous reasoning engine. E.g. Atomspace should contain some atoms and links that can act as CIC (Calculus of Inductive Constructions) language in Coq in which wealth of other logics and programming languages can be encoded. I believe that such formalization of subspace of Atomspace can be done, but for achieving results here and now I am currently going with the combination of Atomspace and Coq. -- 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/081e154d-b58a-4235-82ae-eea6efe0a13f%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.
