Blog:Formal theory, finite model and DL reasoner
|Purpose||Let's discuss the relationship of this 3 powerful things.|
We have 2 statements (Articles below) to discuss. Please comment on them.
This Article is created just typing its URL! Like this http://ontologforum.org/index.php/Blog:Formal_theory,_finite_model_and_DL_reasoner/3_Statement
Henson Graves STATEMENT:
Here are some subtopics of the overall problem of how to realize the axiom set-theory-interpretation paradigm in everyday practice.
1. What is the tradeoff between KR languages in which classification is by sets or types which are terms vs those which classification is represented by predicates?
2. What are the appropriate modular units for reuse?
3. How can formal approaches best exploit graphics based modeling languages?
The paradigm that I am suggesting is exactly the same one that is in John's diagram. For this audience I will stick to logician's terminology. Engineers develop artifacts which are naturally axiom sets even if they don't always recognize it. The axiom sets generate a theory depending on the logic the axiom set is embedded in. The axiom sets are finitely presented. The theory generated by the axiom set are the conclusions which can be derived from the axioms in the logic. As any axiom set or theory there are natural definitions of a valid model of the theory generated by the axiom set. Depending on the axiom set there may possibly be both finite or infinite models. Following John's diagram there are two general kinds of models, the ones in the physical world and simulation models. To me what is important in both cases is not finiteness of the model but its constructivity. This requires a lot more discussion which I will not do here. Following the usual logic paradigm you expect the reasoning to be "true" in all valid models, at least when the theory is sound.
For now only one more idea.
The axioms sets that engineers produce generally have a lot more valid models than the engineer intended. So a lot of practical engineering work is identifying the additional assumptions needed to constrain the valid models. One could view these additional assumptions as "context" for the axiom sets. That is in some domain all of these assumptions could be added automatically to a proof assistant (aka engineer's model development tool) without the axiom set developer even being aware of it. For example in the paper reference above we were modeling both the aircraft and its operational environment. For the axiom set to generate the 3D simulations that we produced we had to add an immense amount of assumptions about physics regarding aerodynamics, sensor performance etc.
Alex Shkotin STATEMENT:
Maxima: "Ontology" is a mirage made by great DL logics in the minds of experts of Expert Systems and WWW.
But ontology, unlike Expert System knowledge, must be presented to public/customer as a text for a universal processor like Protege+Hermit or Jena if you prefer batch mode
Till now the main idea is that
Ontology is a formal text keeping together elements of Formal Theory and Finite Model in a form suitable for Reasoner - usually DL one. A Reasoner can check automatically consistency, perform classification and do other great reasoning services.
To clarify term "engineer's models (aka axiom sets)" let's look at a situation like this: we have
a) a formal theory (some axioms and definitions) for particular application area like "air vehicle model-based design" mentioned by Henson Graves, see .
b) a finite model of theory (a) keeping a particular engineer's model in a DB.
If we need to reason about this (b) model under (a) axioms we convert axioms of formal theory to axioms of OWL-DL and we convert model itself to OWL-DL axioms and this latter set is known as "engineer's models (aka axiom sets)".
The point is that when we work with the finite model itself we need another kind of language (not OWL) to perform "engineering" task: for ex. how many wings do this aircraft have?
And we need a language to handle these models.
These models are finite as they have a finite number of elements. They use numbers but a finite number of them each.
The famous example of a finite model is a graph as still a math object but very useful for modeling. DB is not a math object, unfortunately. If we add a label possibility to graph we should describe it rigorously, and then we may get RDF.
One of the first examples of using the graph as a model is Seven Bridges of Königsberg.
 Air Vehicle Model-Based Design and Simulation Pilot, by Henson Graves, Stephen Guest, Jeff Vermette, Yvonne Bijan, Harold Banks, Greg Whitehead, Bill Ison. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.638.8184
 Seven Bridges of Königsberg. https://en.wikipedia.org/wiki/Seven_Bridges_of_K%C3%B6nigsberg