Regarding the ideas about translation (expression) of PLN into the terms of categorical logics (ideas that are floating around and whose results are pretty much expected and hoped for) everyone is also invited to look at the MMT project - foundation independent logics - by Florian Rabe. MMT is summarized in the "Future of Logics" article http://link.springer.com/article/10.1007/s11787-015-0132-x and the web page of the project itself is https://uniformal.github.io/
While MMT research is very promising, I have some doubts about applicability. Categorical logic represents logics as the categories: terms/expressions are objects and inference relationship forms the set for morphisms. MMT goes one step higher - it defines morphisms among theories (individual logics) therefore one can expect higher order category whose objects are logics and whose morphisms are translation/inheritance relationships among logics (or alternatively - defines similar functors among logics as categories). MMT at the end is something similar like (dependent) type theory and although MMT distances from the meta-logics, MMT still assumes some basic inference rules that are provided extra-linguistically. And although MMT generalizes many algorithms, apparently it still requires to provide those algorithms in the specific cases (they can not be deduced automatically from the syntax and inference rules). So - MMT can be good for the uniform representation of the logics and for smooth transition from one inference type (i.e. rational fair agents) to the other inference type (irrational, narcisstic, greedy agent), but the discovery of logic algorithms is still necessary. I feel that any cognitive system should be capable of using different inference styles and therfore any discovery of Universal Logic could be suitable for the OpenCog. The basic question in this case is: is presentation style of the logic in which every logic can be expressed? There is this question about sequent calculus - http://math.stackexchange.com/questions/2063828/does-every-logic-have-sequent-calculus-if-not-what-are-alternatives-to-them and the answer was no - there still are logics that can no be presented by sequent calculus. My intuition was that ANY type of sequent calculus can be expressed by the forward chaining rules. But that is false - other methods are required. Maybe combination of backward and forward chaining systems fully covers any logic (including nonmonotonic, adaptable logics)? There is apparent need for many specific logics: - e.g. my research are about deontic logics and formalization of norms - this can not be done in the usual first order predicate logics or in the standard modal logics. - e.g. early research by Steunebring (IDSIA) http://people.idsia.ch/~steunebrink/ about formalization of emotions and the BDI agents - e.g. already mentioned formalization of the language by deontic event calculus And it could be nice to arrive at the one reasoning engine that can handle all of then and that enable reasoning in any of them according to the situation. E.g. agents (we) usually have different reasoning styles in math exams, in job and in free time. There is valid suggestion - can we outsource the reasoning part of the OpenCog to some external system, like MMT (I don't know yet about it) or Coq, Isabelle/HOL (as far as I understand those systems are capable to compile formally presented logics (e.g. via rules of sequent calculus) into reasoning engines/provers for those logics (but again - those systems are based on single, bounded meta-logic; to break those bounds is the main aim of MMT)? Or should OpenCog try to outsmart those efforts? And last not least, there is this blog entry http://blog.ruleml.org/post/32629706-the-sad-state-concerning-the-relationships-between-logic-rules-and-logic-programming It is true - many business rules engines lack formal connection to the logic, those rule engines seems to be good heuristics of inferring something from given premises. Maybe OpenCog Rule engine has this formalization that can enable validation and generalization of it. Alex -- 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/10218666-8ee7-46db-95c6-0b1d7c6340f3%40googlegroups.com. For more options, visit https://groups.google.com/d/optout.
