ontolog-forum
[Top] [All Lists]

[ontolog-forum] Hybrid Reasoning Literature / Systems / Model Theory

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Ali SH <asaegyn+out@xxxxxxxxx>
Date: Fri, 30 Nov 2012 21:21:00 -0500
Message-id: <CADr70E1m6sd9rYsvZXw4N8LoEz1vgUVyzcOuS8axywZznzfOKQ@xxxxxxxxxxxxxx>
Hello all,

Ok, this has been sitting in my drafts for a couple of weeks, and I'm really unsure how to frame the question in a coherent way. Anyway, here goes...

I have been working with what I consider hybrid reasoning systems for a couple of years now, but have had difficulty in finding good literature on the topic. Can anyone point me to literature on this front?

Particularly, I have been deploying relatively expressive ontologies using a variety of dbs, algorithms etc. For example, these ontologies may represent geo-spatial reasoning (i.e. generate path from A to B, or tell me what X is beside what Y) or in another domain, relatively complex mathematical analyses (i.e. protein-gene pathway interactions, or relations between entities which involve solving differential equations etc.)

In my current approach, I capture all of these theories in the ontology, but when I have a query that requires "reasoning" in one of these specialized modules, if I can deconstruct the query, I pass off the subpart of the query to the tool best suited for the task (i.e. for the geo-spatial ontology, I would compute path or adjacency using a 3D physics engine). At a very high level, it is similar in many ways to the blackboard approach used in earlier systems. 

In terms of the model theory behind this - is there a name for this approach? I've found some literature touching vaguely similar things, but nothing really satisfying thus far. Moreover, I'm unclear what this entails for the model theory. I currently try to have the implementing reasoning modules sign "semantic contracts" with the sub-theory of the ontology they perform reasoning services for, but in general I cannot guarantee that the axioms in the ontology are always satisfied by the results of the computation in these services. In some cases, the mathematics which are implemented computationally and algorithmically may have theorems for the results, though it's still unclear to me how the implementing algorithm can be guaranteed to satisfy the underlying theory. Unit testing, and competency questions re the expected output are the best I have for most classes of implementation algorithms. To some degree, literature on formal verification of algorithms come close to what i'm looking for, but they rarely connect the results to integrating the algorithms with a broader reasoning system....

A simpler illustrative example might be to represent arithmetic in an ontology (say using Peano's axioms), but to use the built-in functionality provided your favourite programming language to actually perform arithmetic (as opposed to trying to deduce that 1+1=2 based on the axioms in the theory). In cases where I can oversee the implementation of an algorithm, I can try to develop correctness proofs, and also cite literature, but these "semantic contracts" often end up being statistical confidence intervals over a large set of inputs.

Any help or pointers would be greatly appreciated. Or any help in better formulating the problem at hand or which communities to approach.

Thank you kindly,
Ali 



_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J    (01)

<Prev in Thread] Current Thread [Next in Thread>