ontolog-forum
[Top] [All Lists]

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

 To: andrei rodin "henson" Wed, 9 Jul 2014 19:31:23 -0500
 ```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 : 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.    (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) FG > 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) 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.    (016) EJB > 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) 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.    (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) HG > 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) ```
 Current Thread Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, (continued) Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Alex Shkotin Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, John F Sowa Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Alex Shkotin Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Alex Shkotin Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, John F Sowa Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, John F Sowa Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson <= Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Alex Shkotin [ontolog-forum] Predicate Collections for Semantic Relationships, Frank Guerino Re: [ontolog-forum] Predicate Collections for Semantic Relationships, Ravi Sharma Re: [ontolog-forum] Predicate Collections for Semantic Relationships, John F Sowa Re: [ontolog-forum] Predicate Collections for Semantic Relationships, Frank Guerino Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Barkmeyer, Edward J Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, Alex Shkotin Re: [ontolog-forum] Types of Formal (logical) Definitions inontology, henson [ontolog-forum] Semantic Markers in "THE STRUCTURE OF A SEMANTIC THEORY", 1963, John Bottoms