Technical question on Protege

[John F Sowa]

Protege is limited to OWL, which is more complex and more limited than first-order logic.

But I realize that many uses of a type hierarchy do not require the full power of FOL.   My recommendation would be Aristotle's syllogisms for a type hierarchy, supplemented with FOL for a constraint language.  This was the original intention for description logic before the decidability gang restricted its expressive power.

Unfortunately, the constraint of decidability had three results:  (1) it made the language more complex; (2) it seriously limited its expressive power; (3) it made it unusable for a wide range of tools in AI, computer science, and commercial products.  There are many reasoning tools that are more expressive, more powerful, and easier to use than Protege.

For a brief overview of Aristotle's syllogisms, see slides 25 to 30 of https://jfsowa.com/talks/patolog1.pdf 

For more detail about Aristotle and modern logics, see all slides of patolog1.pdf and any references cited on any of those slides.

John

 

---------------------------------------------------------

From: "Mara Abel" <mar...@inf.ufrgs.br>

Colleagues

We are wondering here if we can use the reasoning of Protege to

automatically produce labels for the entities and instances of a domain

ontology.

Any idea about it?

Thank folks!

[Igor Toujilov]

Hi Mara,

Protege does not have the functionality to generate the labels based on reasoning results. The reason for this is that labels are annotation properties which are exempted from reasoning in OWL.

The only way to do this is to develop your own Protege plug-in in Java. But I do not recommend using the idea of generating the labels because of high costs of implementation and maintenance.

There should be another architectural solution for your use case.

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/fec1116b7f674402b604648f23158784%40bestweb.net.

[Polovina, Simon (BTE)]

Hi John and all.

Protégé should have maintained its Frames version. At https://protege.stanford.edu/conference/2006/submissions/slides/7.2wang_protege2006.pdf, there is an insightful presentation that compares Frames and OWL side by side. Notably, the leading industry-strength Enterprise Architecture (EA) tool The Essential Project | Enterprise Architecture Tool (enterprise-architecture.org) uses Protégé Frames under the hood, evidenced by its open-source version. OWL did not fit the bill, as Meta-modelling is important (highlighted in the above presentation link). John, you identified these benefits in your sowazach.pdf (jfsowa.com) 1982 paper with John Zachman, the ‘father’ of EA.

Hence, your remark about OWL’s limitations in commercial products is well-taken.

Simon

[Chris Mungall]

Frames actually turn out to be quite useful for meta-modeling of OWL ontologies. I think we took the wrong fork in the path in 2006, as you suggest.

A lot of large OWL ontologies turn out to be quite unwieldy and difficult to maintain, leading to a lot of different approaches like templated ontology generation from spreadsheets or design pattern systems. See my keynote from the Ontology Pattern Workshop from 2020: doi.org/10.5281/zenodo.7655184

LinkML provides a language with frame-like semantics for a modern user base (YAML rather than S-expressions; compiling to Pydantic and JSON-Schema), and a more user-friendly way to incorporate IRIs for all elements.

We have a framework linkml-owl (https://linkml.io/linkml-owl/) that allows the (historically implicit) metaclasses in an OWL ontology to be modeled in LinkML/frames, with the OWL TBox being "compiled" from LinkML/Frame "instances". This kind of metamodeling is at best very awkward in OWL itself. See the tutorial. 

--

All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/DB8PR03MB549760469F201099256D7620D9802%40DB8PR03MB5497.eurprd03.prod.outlook.com.

[John F Sowa]

Chris and Simon,

Your comments are consistent with widely used development tools that have been implemented.

I agree that frame notation can be quite user-friendly.   But it's important to have a formal specification of exactly how it is mapped to and from FOL or some subset or superset.   Many people throw up their hands when they see predicate calculus notation, but it can be translated to English-like notations with just nine   words: AND, OR, NOT, IF, THEN, EITHER, OR, SOME, EVERY.  (Actually, you only need three words -- AND, NOT, SOME -- but the other words make the sentences shorter and easier to read.)

However, there are many factors that can make implemented systems more user-friendly.  For an overview of the technical issues and examples of various implementations, see https://jfsowa.com/talks/cnl4ss.pdf 

Interesting point:  TQA was a very usable English Query language developed by IBM research.  They found that it was much easier to translate English to predicate calculus notation and then to SQL than to translate directly to SQL.  Formal notations that are good for computers can be good intermediate notations to and from natural languages

In fact, that is an excellent application for LLMs (or more liikely SLMs -- Small Language Models):  translate notations and diagrams with good human factors to and from computer systems..

As the cnl4ss slides show, the users loved TQA, but IBM canceled the project because the task of customizing  TQA for each application was too difficult for most users and too expensive for IBM.  But the current LLM or SLM technology could learn to do the translations very quickly and inexpensively.

I wrote cnl4ss long before LLM/SLM were available.  But today that technology would be excellent for tailoring any of the systems discussed in that pdf.

John

 

---

From: "Chris Mungall" <cjmu...@lbl.gov>

[Kingsley Idehen]

Hi John,

What you've outlined is the strong use-case for LLMs. 

I just wish they weren't marketed as all-answering oracles which isn't an attainable goal due to the very nature of data, information, and knowledge.

-- 
Regards,

Kingsley Idehen	      
Founder & CEO 
OpenLink Software   
Home Page: http://www.openlinksw.com
Community Support: https://community.openlinksw.com
Weblogs (Blogs):
Company Blog: https://medium.com/openlink-software-blog
Virtuoso Blog: https://medium.com/virtuoso-blog
Data Access Drivers Blog: https://medium.com/openlink-odbc-jdbc-ado-net-data-access-drivers

Personal Weblogs (Blogs):
Medium Blog: https://medium.com/@kidehen
Legacy Blogs: http://www.openlinksw.com/blog/~kidehen/
              http://kidehen.blogspot.com

Profile Pages:
Pinterest: https://www.pinterest.com/kidehen/
Quora: https://www.quora.com/profile/Kingsley-Uyi-Idehen
Twitter: https://twitter.com/kidehen
Google+: https://plus.google.com/+KingsleyIdehen/about
LinkedIn: http://www.linkedin.com/in/kidehen

Web Identities (WebID):
Personal: http://kingsley.idehen.net/public_home/kidehen/profile.ttl#i
        : http://id.myopenlink.net/DAV/home/KingsleyUyiIdehen/Public/kingsley.ttl#this

[Alex Shkotin]

Hi Heinrich,

Your point to theoretical knowledge formalization is great. But it is better to formalize existing theories. Of course it is possible to participate in one or another science development, but usually we have a lot of experts there. But knowledge formalization is a special kind of activity. It's like knowledge programming, where we are waiting for marvelous results after putting theoretical knowledge in a computer for algorithmic knowledge processing. 

So let's formalize one or another existing theory. We have this effort in Math like Isabelle, Coq etc. libraries, but not so much in other sciences.

Even Mechanics, just Statics, is not fully formalized.

And we do not formalize theory for themself, because theory is living well without full axiomatization, just using math as much as it needs. We formalize theory to apply it to formal models of one or another part of reality to solve tasks we have there using our powerful computers.

So, what particular theories in which sciences do we have formalized? Axiomatically of course 🙂

Which part of reality do we formally model? Like digital tweens etc.

What kind of tasks can we solve by computer using these formal theories on these formal structures of reality?

Have a look at an example of this triad (theory, structure, task) for such a simple area of math as undirected graphs [1].

Do we have formalized axiomatic theory for Euclid's geometry? Maybe Hilbert's one, but formal. For Planimetry have a look at [2].

Do we have formalized Mechanics? I am on the way to see what it means to get a formal triad for Statics. 

Meanwhile, what about axioms for Genomics?

Best regards,

Alex Shkotin

Independent Computer Scientist ashk...@acm.org

Linkedin ∘ RGate ∘ Academia.edu

Ontolog Board of Trustees https://ontologforum.com/ 

[1] (PDF) Theory framework - knowledge hub message #1

Specific tasks of Ugraphia on a particular structure (formulations, solutions, placement in the framework)

[2] math-formalizations/07_EuclideanGeometry.v at master

ср, 21 авг. 2024 г. в 14:38, Heinrich Herre <heinric...@uni-leipzig.de>:

Hallo together,

I essentially agree with the position of John. Though, I want to clarify two aspects of formal ontology that are permanently ignored.

(1)The greatest and most important application of formal ontology is focussed on aquiring pure knowledge about the world (the reality). For this purpose we developed in our Leipzig Ontology group the onto axiomatic  method. Furthermore, the usage of OWL and even FOL is irrelevant for achieving the main task of (1). The onto-axiomatic method is directed to a) theory formation (developing new theories), b) revision of existing theories, c) developing extensions of theories, d) reconstructing of existing theories.  These analyses and investigations must use a language of greatest expressivity. One may think of at least FOL (First Order Logic), but also logics of higher order, combined with set theory. Actually, set theory can be considered as the universal language for mathematics. Concerning theory formation,  I mention an unsolved problem of formal ontology: Development of a theory that solves Hilbert’s sixth problem (developing the axiomatic foundation for the whole field of physics, with the core problem to unify quantum mechanics and general relativity). If you look in the book „Einstein’s Unfinished Revolution: The search for what lies beyond the Quantum (author Lee Smolin) then you will see in part 3 of this book that these are purely ontological problems. In our interpretation, they are problems that should be investigated in the framework of the onto-axiomatic method. In our Leipzig research program we are developing foundational theories for various domains, among them the cellular level of biology (integrative developmental biology), but also a new theory of space and time, using the ideas of the phenomenologist of Franz Brentano.

(2) What about the usage of OWL, DL,  FOL and other languages? John criticizes the „Decidability Gang“ which restricts the expressive power of FOL to DL (description logic) to get these systems to be decidable. In considering the decision procedure, the complextiy results (with respect to time and space) are permanently ingnored. All the decidability procedures have a high complexity, hence, the insight that a system is decidable, says not so much about the the (time and space) complexity of these algorithms. Most of them are NP-complete, and hence can be  considered as practically unsolvable.

In Summary, the really important and deep problems of formal ontology are related to (1), whereas (2) the restriction to decidable theories (by using DL or OWL) has no real benefit because of he complexity results. I invite the community to work together with us on the problem of the unification physics (Hilbert's sixth problem). The  starting point could be the book by Lee Smolin: Einstein's unfinished revolution.

With kind regards

Heinrich Herre

(Ontology research center of the University of Leipzig,, http://www.onto-med.de)

_________________________________________________________________
To Post:      mailto:iaoa-...@ovgu.de
Msg Archives: https://listserv.ovgu.de/mailman/private/iaoa-member/
List Info:    https://listserv.ovgu.de/mailman/listinfo/iaoa-member/
IAOA website: http://iaoa.org

_________________________________________________________________
To Post:      mailto:iaoa-...@ovgu.de
Msg Archives: https://listserv.ovgu.de/mailman/private/iaoa-member/
List Info:    https://listserv.ovgu.de/mailman/listinfo/iaoa-member/
IAOA website: http://iaoa.org

[John F Sowa]

Heinrich and Alex,

The goal Heinrich summarized is the ultimate goal of mathematical physics.  But I realize that it is a goal that some of the greatest scientists in the world have been working on for the past century.  And I would also like to quote two scientists from the past century:

Einstein:  God does not play dice with the universe.

Niels Bohr:  Stop telling God what to do.

If Einstein, Bohr, and their colleagues and students couldn't solve the problems. I doubt that Ontolog Forum and the other sites listed on this note will do so

I agree with Alex that a smaller, but still vast project would be somewhat more manageable.

Alex:  So let's formalize one or another existing theory. We have this effort in Math like Isabelle, Coq etc. libraries, but not so much in other sciences.  Even Mechanics, just Statics, is not fully formalized...

However, Ontolog forum has over a thousand subscribers, and most of them are not mathematical physicists.  Even those who do have a good background in math & physics have other work to do, and they won't be able to contribute on a daily basis to any such project.

Therefore, I recommend that somebody who does have the time, funding, and interest in this project should set up a mailing list dedicated to it.   Then send a monthly summary of the status  to Ontolog Forum and/or other email lists.

John

[Alex Shkotin]

Heinrich,

1. Thank you. But I was asking not just about axiomatic theory of Mechanics. I have a collection of items and I'll put your reference there. But I was asking about formalized axiomatic theory of Mechanics. As an example of what I am talking about, have a look at Mechanizing Lagrangian Mechanics in Isabelle/HOL.
   Considering we are talking about axiomatic theory of Geometry, we may refer to Euclid's text, Hilbert's one, and there are more of nice Geometry axiomatizations. But give me, please, an example of formalization of those theories. I have only one.

2. About GFO. Following "The "native" formalization language for GFO is first-order logic (FOL). Partial axiomatizations of GFO in FOL exist in report working drafts, but are not yet available to the public."see, full formalization is not finished yet?

Formalization is a next level of accuracy even for mathematicians🎯 

Alex

пт, 23 авг. 2024 г. в 18:56, Heinrich Herre <heinric...@uni-leipzig.de>:

Hallo together,

two further remarks.

(1) There was the question about the axiomatization of classical mechanics. There is such an axiomatization, elaborated by the logician Hans Hermes. (Eine Axiomatisierung der allgemeinen Mechanics. Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften, Leipzig, 1938, 48 pp.)

(2) An ontologial foundation of quantum mechanics is simpler than the unification of quantum mechanics and general relativity.. There are, of course,various different interpetations of quantum mechanics. We are working on an overarching framework for the quantum theory form which various interptetations and resuls can be derived. We need, I believe, a deeper understanding of the duality between particle and wave. We discovered that behind this phenomenon there is a deeper duality, that between object and process. The relation between these kinds of entities is expressed by the integration axiom of GFO (General Formal Ontology). Let us see, what we will get. I will inform you about our results. Or approach is compatible with that of David Bohm.

With best wishes

Heinrich

Am 23.08.2024 um 15:58 schrieb Heinrich Herre:

Hallo together,

I know, of course, that my proposal is a bit provocative. I wanted to hint that the onto-axiomatic method allows an access to the understanding of this problem. This problem can be reduced to another problem: Quantum mechanics needs time quants (and space quants), on the other hand, general relativity assumes the continuity of time and space. How these completely different structures can be unified? We developed a new theory of time and space, based the ideas of Franz Brentano, and hopefully these new models allows constructions of new type. I had some years ago contacts to top physicists, they never heard something about Brentano's approach. Sometimes scientists are living an a bubble of conventional standard notions. The onto-axiomatic method provides methods to break such bubbles. We are working on this problem, let us see what we get.

With best wishes

Heirich

From: "Alex Shkotin" <alex.s...@gmail.com>

(1)The greatest and most important application of formal ontology is focussed on aquiring pure knowledge about the world (the reality). For this purpose we developed in our Leipzig Ontology group the onto axiomatic  method. Furthermore, the usage of OWL and even FOL is irrelevant for achieving the main task of (1). The onto-axiomatic method is directed to a) theory formation (developing new theories), b) revision of existing theories, c) developing extensions of theories, d) reconstructing of existing theories.  These analyses and investigations must use a language of greatest expressivity. One may think of at least FOL (First Order Logic), but also logics of higher order, combined with set theory. Actually, set theory can be considered as the universal language for mathematics. Concerning theory formation,  I mention an unsolved problem of formal ontology: Development of a theory that solves Hilbert’s sixth problem (developing the axiomatic foundation for the whole field of physics, with the core problem to unify quantum mechanics and general relativity). If you look in the book „Einstein’s Unfinished Revolution: The search for what lies beyond the Quantum (author Lee Smolin) then you will see in part 3 of this book that these are purely ontological problems. In our interpretation, they are problems that should be investigated in the framework of the onto-axiomatic method. In our Leipzig research program we are developing foundational theories for various domains, among them the cellular level of biology (integrative developmental biology), but also a new theory of space and time, using the i deas of the phenomenologist of Franz Brentano.

(2) What about the usage of OWL, DL,  FOL and other languages? John criticizes the „Decidability Gang“ which restricts the expressive power of FOL to DL (description logic) to get these systems to be decidable. In considering the decision procedure, the complextiy results (with respect to time and space) are permanently ingnored. All the decidability procedures have a high complexity, hence, the insight that a system is decidable, says not so much about the the (time and space) complexity of these algorithms. Most of them are NP-complete, and hence can be  considered as practically unsolvable.

In Summary, the really important and deep problems of formal ontology are related to (1), whereas (2) the restriction to decidable theories (by using DL or OWL) has no real benefit because of he complexity results. I invite the community to work together with us on the problem of the unification physics (Hilbert's sixth problem). The  starting point could be the book by Lee Smolin: Einstein's unfinished revolution.

With kind regards

Heinrich Herre

[Alex Shkotin]

Heinrich,

Following "We developed a new theory of time and space" is it possible to read it?

What is the form your theory exists in?

Let me propose to keep it in a knowledge hub form of framework. Like for ugraph theory here.

Today when we have GenAI as an alternative knowledge concentrator we at least know that it is possible to put ALL our theoretical knowledge in one "computer". But this must be done through the formalization of accumulated verified theoretical and technological knowledge, and not through training✈️

Alex

пт, 23 авг. 2024 г. в 16:58, Heinrich Herre <heinric...@uni-leipzig.de>:

Hallo together,

I know, of course, that my proposal is a bit provocative. I wanted to hint that the onto-axiomatic method allows an access to the understanding of this problem. This problem can be reduced to another problem: Quantum mechanics needs time quants (and space quants), on the other hand, general relativity assumes the continuity of time and space. How these completely different structures can be unified? We developed a new theory of time and space, based the ideas of Franz Brentano, and hopefully these new models allows constructions of new type. I had some years ago contacts to top physicists, they never heard something about Brentano's approach. Sometimes scientists are living an a bubble of conventional standard notions. The onto-axiomatic method provides methods to break such bubbles. We are working on this problem, let us see what we get.

With best wishes

Heirich

Am 22.08.2024 um 22:14 schrieb John F Sowa:

From: "Alex Shkotin" <alex.s...@gmail.com>

(1)The greatest and most important application of formal ontology is focussed on aquiring pure knowledge about the world (the reality). For this purpose we developed in our Leipzig Ontology group the onto axiomatic  method. Furthermore, the usage of OWL and even FOL is irrelevant for achieving the main task of (1). The onto-axiomatic method is directed to a) theory formation (developing new theories), b) revision of existing theories, c) developing extensions of theories, d) reconstructing of existing theories.  These analyses and investigations must use a language of greatest expressivity. One may think of at least FOL (First Order Logic), but also logics of higher order, combined with set theory. Actually, set theory can be considered as the universal language for mathematics. Concerning theory formation,  I mention an unsolved problem of formal ontology: Development of a theory that solves Hilbert’s sixth problem (developing the axiomatic foundation for the whole field of physics, with the core problem to unify quantum mechanics and general relativity). If you look in the book „Einstein’s Unfinished Revolution: The search for what lies beyond the Quantum (author Lee Smolin) then you will see in part 3 of this book that these are purely ontological problems. In our interpretation, they are problems that should be investigated in the framework of the onto-axiomatic method. In our Leipzig research program we are developing foundational theories for various domains, among them the cellular level of biology (integrative developmental biology), but also a new theory of space and time, using the i deas of the phenomenologist of Franz Brentano.

(2) What about the usage of OWL, DL,  FOL and other languages? John criticizes the „Decidability Gang“ which restricts the expressive power of FOL to DL (description logic) to get these systems to be decidable. In considering the decision procedure, the complextiy results (with respect to time and space) are permanently ingnored. All the decidability procedures have a high complexity, hence, the insight that a system is decidable, says not so much about the the (time and space) complexity of these algorithms. Most of them are NP-complete, and hence can be  considered as practically unsolvable.

In Summary, the really important and deep problems of formal ontology are related to (1), whereas (2) the restriction to decidable theories (by using DL or OWL) has no real benefit because of he complexity results. I invite the community to work together with us on the problem of the unification physics (Hilbert's sixth problem). The  starting point could be the book by Lee Smolin: Einstein's unfinished revolution.

With kind regards

Heinrich Herre

[Nadin, Mihai]

Why not?

Just wondering.

Mihai Nadin

Get Outlook for iOS

---

From: ontolo...@googlegroups.com <ontolo...@googlegroups.com> on behalf of Alex Shkotin <alex.s...@gmail.com>
Sent: Saturday, August 24, 2024 3:22:23 AM
To: [IAOA-member] <iaoa-...@ovgu.de>
Cc: ontolo...@googlegroups.com <ontolo...@googlegroups.com>
Subject: [ontolog-forum] Re: [iaoa-member] Technical question on Protege

 

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROTBEfL0ROSih%2BfWwQFH2o4RQNNJ3S6sGTOwO-%2BjRVX_eg%40mail.gmail.com.

[John F Sowa]

First-order logic is a universal format that has been used to define every digital device of any kind and anything that can be implemented on any digital computer.  Furthermore, every logician in the world and everybody who has studied logic knows FOL.

Alex:  Let me propose to keep it in a knowledge hub form of framework. Like for ugraph theory here.  Today when we have GenAI as an alternative knowledge concentrator we at least know that it is possible to put ALL our theoretical knowledge in one "computer".

No, no, no absolutely NOT!   Only a tiny fraction of logicians have ever seen ugraph.

Only until there is a formal translation to and from FOL, we have ZERO evidence that ugraph is precise and reliable.  And if anybody can demonstrate that such a translation is possible, then that is a proof that we don't need ugraph.  We can continue to use FOL.

But there is also a standard for the superset of FOL called DOL, which is an official standard of the Object Management Group.  For a summary of the DOL standard, see slides 8 to 12  of  https://jfsowa.com/talks/eswc.pdf .  That talk (with a subset of the slides) won the best presentation award at the 2020 European Semantic Web Conference.

For the complete specification of the Distributed Ontology, Modeling, and Specification

Language, see https://www.omg.org/spec/DOL/1.0

And GenAI is notorious for its errors and hallucinations.  It is not a good recommendation for anything that requires absolute precision and reliability.

John

 

---

From: "Nadin, Mihai" <na...@utdallas.edu>
Sent: 8/24/24 4:32 PM

Why not?

Just wondering.

Mihai Nadin

Get Outlook for iOSFrom: ontolo...@googlegroups.com <ontolo...@googlegroups.com> on behalf of Alex Shkotin <alex.s...@gmail.com>

Sent: Saturday, August 24, 2024 3:22:23 AM

[Alex Shkotin]

John,

It's a misunderstanding. Theory and practice of ugraph is taken just as an example of very simple math structure (undirected graph) and very simple and not First-Order Logic theory for this kind of structure.  We need just one finite set U of beings (both edges and nodes) and one binary finite relation inc on it, for predicate: being-1 is incident to being-2.

And the number of axioms is just two:

First of them claims that relation inc is on U.

Second, that the predicate inc must be splitted and one-two-left one.

How to keep theory about some kind of structures in a framework, and how to keep tasks on these structures and solutions of these tasks, applying our theoretical knowledge; this is what [1] about.

Both frameworks (for theory and for tasks) are indifferent to any kind of formalizations, just keeping all formalizations for this particular unit of knowledge together in one place.

Consider for example the definition of what it means for a binary relation to be incident.

incident eng:incident rus:инцидентно

rus	Пусть R есть ботн. R инцидентно если и только если R расщеплено и раз-два-слева.
eng	Let R be a binary relation. R is incident if and only if R is split and one-two-left.
yfl	decl incident (TV frel(Ide Ide))(R) ≝ splitted(R) ∧ left12(R)
fl0	???

Give to Admin a formalization on CL, CASL, OWL2 etc. and he put it there as a new line.

And the idea of undirected graphs is famous thanks to Euler: Seven Bridges of Königsberg - Wikipedia.

So, we need two frameworks: one for theory, another for tasks.

Formalization language may be any.

For example YAFOLL is not FOL as it possible to write there

∀e:R (#y:R e(1)=y(1))≤2

And quantity quantifier # is not from FOL.

Any language from the DOL family may be used in framework.

The super-task is theoretical knowledge concentration, not language competition.

Alex

[1] https://www.researchgate.net/publication/374265191_Theory_framework_-_knowledge_hub_message_1

https://www.researchgate.net/publication/380576198_Specific_tasks_of_Ugraphia_on_a_particular_structure_formulations_solutions_placement_in_the_framework

вс, 25 авг. 2024 г. в 00:48, John F Sowa <so...@bestweb.net>:

--
All contributions to this forum are covered by an open-source license.
For information about the wiki, the license, and how to subscribe or
unsubscribe to the forum, see http://ontologforum.org/info
---
You received this message because you are subscribed to the Google Groups "ontolog-forum" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-foru...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/05191368d0db4a2ba74a670b2318d594%40bestweb.net.

[Alex Shkotin]

Dear Heinrich,

Let me first put one point and then I'll answer inline step-by-step.

The point "Storing the theory of a particular subject area in one place and maintaining it (including formalization) through collective efforts is easily possible with the modern development of technology. The concentration and verification of knowledge achieved in this case should give a powerful ordering of theoretical knowledge, which will facilitate their formalization, i.e. mathematical notation, and therefore algorithmic processing in many cases, up to the semi-automatic proof of various kinds of consequences, for example, theorems. This message describes what the framework of the theory is, intended for unified storage and collective accumulation of its results." see

Now inlines:

вс, 25 авг. 2024 г. в 16:09, Heinrich Herre <heinric...@uni-leipzig.de>:

Dear Alex,

we should clarify the basic notions, you are using. If you are speaking about axiomatizations, is there a relation to Isabelle/HOL?

Yes. And they have a formal theory of ugraph (their term🏋️). If we have a framework for ugraphia the author of Isa/HOL theory can place it there.

Should the axiomatization be formalized within the Isabelle/HOL-formalism? This is a theorem-prover and there are some of them, for example Vampire developd by Voronkow. There is the general idea to solve problems automatically by using a theorem prover. Automatic theorem proving is an important field of AI and I am thinking about integrating LLM (Large Language Models- based on inductive inference) with formal logic and deduction. I call such systems (they do not yet exist) OntoLLMs. Further, there should be no problem to transform a first order theory  into the Isabelle/HOL formalism (or Vampire formalism). Further, you should use the standard notions for graphs (of binary relations). You are speaking about undirected binary relations, which can be visually presented as graphs. The graphs, you  mentioned, do they have the valancy at most two? If you need some results on the coplexity of graphs (decidability undecidabiity) I may offer many of them.

With best wishes

Heinrich

_________________________________________________________________
To Post:      mailto:iaoa-...@ovgu.de
Msg Archives: https://listserv.ovgu.de/mailman/private/iaoa-member/
List Info:    https://listserv.ovgu.de/mailman/listinfo/iaoa-member/
IAOA website: http://iaoa.org

[Alex Shkotin]

APOLOGIZE for the wrong key-stroke!

Please see the full version🏋️

---------- Forwarded message ---------
От: Alex Shkotin <alex.s...@gmail.com>
Date: пн, 26 авг. 2024 г. в 10:40
Subject: Re: [iaoa-member] [ontolog-forum] DOL standard by the Object Management Group (was Technical question on Protege
To: [IAOA-member] <iaoa-...@ovgu.de>, ontolog-forum <ontolo...@googlegroups.com>
Cc: Heinrich Herre <heinric...@uni-leipzig.de>

Dear Heinrich,

Let me first put one point and then I'll answer inline step-by-step. The point is "Storing the theory of a particular subject area in one place and maintaining it (including formalization) through collective efforts is easily possible with the modern development of technology. The concentration and verification of knowledge achieved in this case should give a powerful ordering of theoretical knowledge, which will facilitate their formalization, i.e. mathematical notation, and therefore algorithmic processing in many cases, up to the semi-automatic proof of various kinds of consequences, for example, theorems. This message describes what the framework of the theory is, intended for unified storage and collective accumulation of its results."

Now inlines:

вс, 25 авг. 2024 г. в 16:09, Heinrich Herre <heinric...@uni-leipzig.de>:

Dear Alex,

we should clarify the basic notions, you are using. If you are speaking about axiomatizations, is there a relation to Isabelle/HOL?

AS: Yes. And they have a formal theory of ugraph (their term🏋️). If we have a framework for ugraphia the author of Isa/HOL theory can place it there.

Should the axiomatization be formalized within the Isabelle/HOL-formalism?

AS: Any axiomatization is welcome in the framework. 

This is a theorem-prover and there are some of them, for example Vampire developd by Voronkow. There is the general idea to solve problems automatically by using a theorem prover. Automatic theorem proving is an important field of AI and I am thinking about integrating LLM (Large Language Models- based on inductive inference) with formal logic and deduction. I call such systems (they do not yet exist) OntoLLMs.

AS: I doubt that theorem prover can solve any task of calculation, and most engineering tasks are direct calculations. But of cause any derivation needed must be automatic as much as possible.

For example in mechanics we should derive from the system description that it's static.

"Large Language Models- based on inductive inference" sounds very interesting. How do you train them?

Further, there should be no problem to transform a first order theory  into the Isabelle/HOL formalism (or Vampire formalism).

AS: FOL is just part of HOL. We do not need any transformation.

Further, you should use the standard notions for graphs (of binary relations).

AS: Yes. Vertex, Edge are standard. But Incident relation is a little bit not: only edge may be incident to node. I don't think this is a big problem.

You are speaking about undirected binary relations, which can be visually presented as graphs. The graphs, you  mentioned, do they have the valancy at most two?

AS: Yes.

If you need some results on the coplexity of graphs (decidability undecidabiity) I may offer many of them.

AS: Great. When we create a framework for ugraphs we can put them there. Or, what about your team would begin this framework? For all humanity?

With best wishes

Alex