Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

[Alex Shkotin <alex.shkotin@xxxxxxxxx>]

Henson,

HG:

"Benzene is a good example test case for an ontology language. The idea is to give an axiom set in a logic for the class of benzene molecules.  Then use automated reasoning answer questions about the structure of benzene molecules. For example, one would like to ask in the ontology language the question “whether any benzene molecule has a carbon ring? “... Reasoning on DL axiom sets cannot answer this question correctly..."

But there is another equivalent question, I think DL-ed:  “whether any benzene molecule has a carbon ring with length <13?“ 

HG:

"However, one can give first order axioms for Benzene which constrain all the models to consist of molecules which only have the correct shape.  This is not a trivial result."

I am sure that Benzene definition is DL-ed too. I am just wating for experts answer. It's summer you know.

​​

Alex

2014-07-10 4:31 GMT+04:00 henson <henson.graves@xxxxxxxxxxx>:

Indeed category theory is a mathematical formalism which is being used for ontology, even in cases where the users are unaware of it. The reasons are straight forward. A category is really a directed graph with a path composition operation and possibly other language constructions. Many applications in science and engineering make heavy use of directed graphs, including John’s bridge example in more ways than one.

Benzene is a good example test case for an ontology language. The idea is to give an axiom set in a logic for the class of benzene molecules.  Then use automated reasoning answer questions about the structure of benzene molecules. For example, one would like to ask in the ontology language the question “whether any benzene molecule has a carbon ring? “ Automated reasoning can give the correct answer only when all of the benzene molecules in any valid interpretation have the structure such as is shown in the diagram :
image: http://media1.picsearch.com/is?8Pu5G3VX2yKV0e-u-4aq4q12Q8DGv_UKZslfRR_RSLM&height=254
Reasoning on DL axiom sets cannot answer this question correctly, as the DL axioms will always have a tree structured model which does not conform to this picture. Remember, the diagram and the axiom set are description templates, rather than descriptions of a specific molecule.

However, one can give first order axioms for Benzene which constrain all the models to consist of molecules which only have the correct shape.  This is not a trivial result. I repeat the comment that  approach separates the logical language used to express the axioms from the logic’s term language which is the ontology language.  The logical langauge is classical first order, the term language may or may not be classical

A category theory can be used as an ontology language by giving FOL axioms for the language constructions such as path composition. One needs a bit more ontology language constructions than a directed graph for this example, but not a lot.  The axioms use two sorts, nodes and arrows. I will call them types and maps. A category theory person would call them objects and maps. Some of this was noted in some of the earlier exchanges with Alex. The axioms for composition are of course partial, as has been commented on before. But as the conditions for composition to be well defined are decidable, there really is no problem with proof theory or model theory.

The axioms for a category or directed graph with path composition can be found in the Lambek and Scott book in the early pages. Of course a category can be very large, but in engineering examples generally have finite models. For example  the benzene description with the right constructions generates a category which has a canonical minimal finite model which looks like the graphs one sees in Wikipedia.

With regard to whether predicates are viewed as a form of classification, I would say yes. But there is an important caveat. There are two logics involved. One is the logic in which the axiom set is expressed which is called the external logic. The other is that in  a category with additional structure such as a Cartesian close category or elementary topos, there is an internal logic. These frameworks have a type constant symbol Omega. An internal formula is a map q:X  → Omega. If Omega reduces to {true,false} then the internal logic looks like the external one. However, one can add truth value constants in addition to true:X →  Omega, and false:X  →  Omega such as maybe:X → Omega. Then one gets a non-traditional logic.  Type theory, and rule systems such as Hilog, use this device of  having an internal representation of higher order logic as terms within a first order presentation logic. The internal logic admits various generalization of classical logic.  The external predicates classify the terms, i.e., syntactic structures. The internal predicates classify things in the interpretation.  As an example of this idea, the external predicates allows one to deduce that “the gun shot hit the target = maybe”. The statement is an internal formulae and the equation is external.

I would modify John’s comment slightly. If you have to ask what it is from the viewpoint of ontology, the worst place to find out are standard text books on category theory. The reason for this is it is usually presented as a theory within set theory, rather than as a first order theory. Presenting topos theory as a theory within set theory obviates ability to serve as an ontology language.

By the way, the signature of the Benzene axiom set, as I would do it, has 3 type symbol constants, Benzene, Hydrogen and Carbon. It also has 12 part maps, and 12 type constructions, and 12 connection maps.  I have not, of course, indicated what the axioms are which are needed for the benzene axiom set.

Henson Graves

-----Original Message----- From: John F Sowa

Sent: Wednesday, July 09, 2014 12:01 PM

To: ontolog-forum@xxxxxxxxxxxxxxxx
Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions inontology

Frank, Henson, and Ed,

FG

Given the discussions on Category Theory, I was curious if the
community views Predicates as a form of categorization/classification.

Two points:

 1. Category theory is a mathematical system that might be used for
    ontology.  But if you have to ask what it is, don't use it.
    Brief summary:  http://en.wikipedia.org/wiki/Category_theory

 2. Every class, type, or category in any ontology can be associated
    with a predicate that is true of everything in the class, type,
    or category and false of everything not in it.

HG

I believe the problem is that OWL axiom sets always have a tree
model whether you want it or not. OWL axiom sets may have other
models which are not trees.

EJB

Not quite 'trees' -- classification lattices, with 'property links'
that produce more or less general semantic networks, including cycles.

I agree with Henson.  The OWL *classes* are organized in lattices.
But the *models* (in Tarski's sense) are limited to trees.

For example, a benzene ring has a cycle.  OWL cannot state the
critical properties that require a model of benzene to have a cycle.

Just look at any bridge truss, and you'll find interconnected
triangles that create huge numbers of cycles.  It's impossible
to find any complex artifact or biological system without cycles.
OWL cannot specify, analyze, or reason about those cycles.

HG

Where they have problems is in constructing OWL axiom sets for
a molecule such as H2O which constrains the models to only consist
of molecules with exactly three atoms. There are a lot of papers
by Horrocks and Motik and students on this topic.

I know Horrocks and Motik.   They're intelligent, but they're
hopelessly *arrogant* to claim that they are qualified to tell
experts in every branch of science, engineering, and business
what models they're allowed to use, represent, and reason with.

HG

This has led them to try graph extensions of DL and logic
programming extensions.

Yes.  And every one of those extensions adds more and more complexities
to an overly complex system.  By comparison, the LP systems are easier
to learn and use and far more efficient for equivalent applications.

Programmers and computer scientists have had far better methods
for controlling complexity and avoiding issues of undecidability.
They use various terms:  structured programming, structured
analysis, design patterns, and knowledge compilers.

When I wrote my article "Fads and Fallacies in Logic", the primary
fad I had in mind was OWL.  And the primary fallacy was decidability
as the bogeyman:  http://www.jfsowa.com/pubs/fflogic.pdf

By the way, Jim Hendler was the editor of the journal in which it
was published.  And he liked that article very much.

John

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@ontolog.cim3.net
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

_________________________________________________________________
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)