[Top] [All Lists]

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

To: <ontolog-forum@xxxxxxxxxxxxxxxx>
Cc: andrei rodin <andrei@xxxxxxxxxxxxxxx>
From: "henson" <henson.graves@xxxxxxxxxxx>
Date: Wed, 9 Jul 2014 19:31:23 -0500
Message-id: <BLU176-DS490B21CAEBE4CE14987BFE40E0@xxxxxxx>
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.    (01)

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 :
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.    (02)

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    (03)

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.    (04)

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.    (05)

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.    (06)

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.    (07)

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.    (08)

Henson Graves    (09)

-----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    (010)

Frank, Henson, and Ed,    (011)

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

Two points:    (013)

  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    (014)

  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.    (015)

> 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.    (016)

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

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

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

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.    (020)

> 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.    (021)

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.    (022)

> This has led them to try graph extensions of DL and logic
> programming extensions.    (023)

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.    (024)

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.    (025)

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    (026)

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

John    (028)

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    (029)

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    (030)

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