Tools for modeling in first-order logic - making conceptual/ontological models in FOL
Knowledge representation
Alex Shkotin
Thank you for your nice questions. For me FOL is an Assembler of KR. And I am for HOL. So I asked Gemini to help me to answer your questions.
What user-friendly* tools capable of handling full first-order logic do you know?
AS:Any kind of HOL IDE and languages is a user-friendly tool fully or partially handling FOL.
For example
Coq Integrated Development Environment — Coq 8.12.2 documentation
https://isabelle.in.tum.de/installation.html
etc.
Gemini: What user-friendly tools capable of handling full...
What tools can you build a conceptual model, ontology in FOL?
AS:The same plus http://attempto.ifi.uzh.ch/site/
Gemini: What tools can you build a conceptual model, onto...
What is a stack for: translating natural language sentences into FOL and then FOL to a computable language?
AS:Attempto Controlled English (ACE)
Gemini's answer is not interesting.
If you refer to a particular FOL computable language, such as KIF, CL, or otherwise, what tools can easily help make an ontology formalized in the given langauge?
AS: Let me hope http://hets.eu/
Gemini: If we refer to a particular FOL computable langua...
Alex
--
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/ac5c66d7-6ea7-4554-9cad-50777f899bd4n%40googlegroups.com.
John F Sowa
Ítalo Oliveira
--
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/4c5a62a0868b416a815d2b1e2f7f0432%40bestweb.net.
Alexandre Rademaker
Ítalo, thank you for mentioning Lean. I was surprised that Lean had not been discussed before. People can see my formalization in the Lean of the Agatha puzzle to see what it looks like. In this particular code, I am basically encoding FOL formulas in Lean.
https://github.com/arademaker/puzzles/blob/main/Puzzles/Basic.lean
The original implementation is the TPTP collection, https://tptp.org/cgi-bin/SeeTPTP?Category=Problems&Domain=PUZ&File=PUZ001+1.p.
I am working now on the automatic translation from the natural language text to Lean using a traditional grammar-based approach for semantic parsing, mainly motivated by this text from Geoff: https://aarinc.org/Newsletters/141-2023-06.html#geoff.
Best,
Alexandre
David Eddy
Ítalo
Chris Mungall
--
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/ac5c66d7-6ea7-4554-9cad-50777f899bd4n%40googlegroups.com.
Alex Shkotin
--
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/4c5a62a0868b416a815d2b1e2f7f0432%40bestweb.net.
Alex Shkotin
Ítalo,
Is there any ontology in Lean, i.e. formal theories and their models?
Alex
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAOEC0q-HOZ76eaqGf3iaDpfS6XpR3KwGDKH264Ut71X%2BpFtqHw%40mail.gmail.com.
Alex Shkotin
Alexandre,
What kind of texts do you keep in mind to translate?
If these are about undirected graph theory and structures, I am ready to add both to theory and task frameworks.
And you may add Lean lines to any framework unit of knowledge. Like this
Give me a Lean definition of "degree of a vertex v in a graph g" and I put it in the framework with pleasure.
The place is ready 🏹
If you are working on another theoretical knowledge - which one?
Alex
--
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/B4C005C2-E66D-4217-8C15-04FE3236A4E9%40gmail.com.
Ítalo Oliveira
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROSAyqQRbW12O99iutH0xj%2B2-tyD%3D5Q-8HEdaZwj%3DG18Lw%40mail.gmail.com.
Alexandre Rademaker
Depends on what you call formal theories! Besides the incredible work from mathematicians in the https://leanprover-community.github.io/mathlib-overview.html. We also have initial works on other domains, such as chemistry; see https://arxiv.org/abs/2210.12150.
Of course, mathematicians use Lean with a very different mindset. For a mathematician, "Axioms are dangerous because they can lead to an inconsistent logic, in which we can derive False.” [1].
Another critical difference for me is that in dependent types, we have many different approaches to encoding the notion of hierarchy, the is-a relationship. This flexibility is good and bad; there is no single way to encode the idea.
Best,
Alexandre
[1] https://github.com/blanchette/interactive_theorem_proving_2024/raw/main/hitchhikers_guide_2024_lmu_desktop.pdf
Alexandre Rademaker
I agree Ítalo. I see many benefits, but I usually emphasize two. First, using the same language for expressions (in dependent types, we don’t distinguish between terms and formulas; formulas are terms of type Prop) and proofs. Second, the ability to define computable functions. Lean is a functional programming language and not only an interactive theorem prover.
For instance, in SUMO we have an axiomatization of the function `floor`
https://sigma.ontologyportal.org:8443/sigma/Browse.jsp?lang=EnglishLanguage&flang=SUO-KIF&kb=SUMO&term=FloorFn
and the axiomatization of the `first` for the first element of a list:
https://sigma.ontologyportal.org:8443/sigma/Browse.jsp?lang=EnglishLanguage&flang=SUO-KIF&kb=SUMO&term=FirstFn
In the old days of SNARK from SRI (https://www.ai.sri.com/~stickel/snark.html), we have the “procedural attachment” (see https://www.sri.com/wp-content/uploads/2021/12/784.pdf). In modern SMT, the systems have some theories built into the tool.
Does can be defined in Lean and evaluated, not axiomatized. Because we have the full power of Calculus of Constructions. More at https://docs.lean-lang.org/theorem_proving_in_lean4/.
I hope that makes sense.
Best,
Alexandre
Ravi Sharma
--
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/ac5c66d7-6ea7-4554-9cad-50777f899bd4n%40googlegroups.com.
alex.shkotin
Chris,
Never heard that reasoning can be done in Python. Too bad I don't know Python. I'll do it and make a line for it in the ugraph theory framework when I get to paths. Path has a rather subtle definition. And path is an entity on its own where your Path is actually a predicate of path existence.
And following [GNaA] 1.3 we have to define "walk" first, then "trail", and then "path" as a property of sequence of vertices and nodes.
And your two axioms
are theorems in ugraph theory.
We have a polymorphic predicate adjacent where you use Link. With definition:
Calculation on the model of logical formulas is clear to me. Especially if we specify how to encode quantifiers, but I'll definitely look at reasoning.
Very interesting!
Alex
Alex Shkotin
Alexandre,
Thank you! Great references. Must read.
Alex
--
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/4615BDB3-6BB1-49A6-AF58-F956BDDF64A2%40gmail.com.
John Singer
Chris Mungall
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/22a5fd29-f005-40f5-bcdd-2024b3f7b0ban%40googlegroups.com.
Chris Partridge
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAN9Aifs6%3Dqnga%3DH%3D0rw-9J7rnCv_Rp9WRx-K2xwxxVAZcBSyQQ%40mail.gmail.com.
John F Sowa
Chris Mungall
@chris_mungall - apologies if you answered earlier, but what 'format' are you using to input the FOL axioms? TPTP? CLIF?
(The reason I'm asking is we did some work a while ago and we found it useful to have a more human-readable input format - we went with CLIF using an EBNF grammar approach to read - converted to an internal model then output in whatever format needed - often TPTP for e.g. Vampire. One of the design questions that came up was what was the best way to consume (effectively unstructured) text FOL 9e.g. a csv) at scale - and then what a common data structure that could output a variety of formats would look like.)
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAMWD8MrFo2LNNPa9f0fi6BegQKXVXVwtfsNzuymb1-zow_oauQ%40mail.gmail.com.
Ravi Sharma
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAN9AifsHJzC0w6965_pNEnNNWoSxLH0%2BSYGhHLh0bTB1Qnvzfw%40mail.gmail.com.
John F Sowa
Ravi Sharma
--
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/acdfeb3300c7448daf921ce09978681b%40bestweb.net.
Polovina, Simon (BTE)
Hi all!
Connecting the Facts: SAP HANA Cloud’s Knowledge G... - SAP Community may interest you. Combining knowledge graphs with LLM as a commercial product by the business computing market leader, SAP.
Simon
Dr Simon Polovina
Department of Computing, Sheffield Hallam University, UK
Ítalo Oliveira
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAAN3-5enHB4F_n4LuF91M0Wz8Yn9r2dhG%3DYorCvdmbmHPe7G6Q%40mail.gmail.com.
Alex Shkotin
Chris and ALL,
It may be interesting to consider a complex unit of knowledge within a theory - a proof.
For example:proof Pr1_1__1 Th1_1
Here we have a sequence of statements in one language or another. Moreover, the subsequent statement is obtained from the previous ones according to the rule specified in the last column. As described here. And here it is important to emphasize that although in general this sequence is the same as a proof in mathematical logic, the rules applied are taken from practice.
The structure and functionality of the theory framework is an RFC on the way to launching a project for such a repository.
Alex
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAN9Aifs6%3Dqnga%3DH%3D0rw-9J7rnCv_Rp9WRx-K2xwxxVAZcBSyQQ%40mail.gmail.com.
Alex Shkotin
ChrisP,
You are describing an interesting project in which, as far as I understand, some knowledge is recorded in a language defined by a context-free grammar in EBNF notation. What tool did you use to build parsers? Antlr?
And the language itself? Is it a subset of natural language or some formal one?
Let's say the input language is a subset of English. Where do you translate it? We once translated it into OWL2 using APE.
Is there a description of the project?
Very interesting.
Alex
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/CAMWD8MrFo2LNNPa9f0fi6BegQKXVXVwtfsNzuymb1-zow_oauQ%40mail.gmail.com.
Alex Shkotin
JFS:"To Alex: There is no need for you (or anybody else) to lean Python. With the DOL standard, any syntax that conforms to the ISO standard for Common Logic can be automatically translated to and from any syntax that can express FOL or many subsets and supersets of FOL. That includes OWL, Turtle, UML, and even TPTP (Thousands of Problems for Theorem Provers)."
The situation is just the opposite. Formalization of a unit of knowledge (in this case, two theorems) can be placed in the framework of the theory (exactly this one!) in any language. The main thing is that there are enthusiasts who undertake to formalize this particular theory in this particular formal language. And whether it will be a language from the DOL family or Python is the choice of enthusiasts.
The beauty of formalizing a unit of knowledge is that they are usually small (definitions can be several sentences long), of course, except for proofs that can take up terabytes (but in this case it's initially formal). The main thing is that the new unit is consistent with those already in the framework. This structure of the framework of the theory is known but not simple.
Let's assume that we already have two such units of knowledge in the framework, definitions for Link, Path. Then we need to add two more units of knowledge: theorems
in some formal language - the one CP asked about.
And so, Python lines will need to be added to the framework for them into the same knowledge units. Probably these
def path_from_link(x: ID, y: ID):
assert Link(source=x, target=y) >> Path(source=x, target=y, hops=1)
def transitivity(x: ID, y: ID, z: ID, d1: int, d2: int):
assert ((Path(source=x, target=y, hops=d1) & Path(source=y, target=z, hops=d2)) >>
Path(source=x, target=z, hops=d1+d2))
But Python is a delicate matter - the indentation is important, the environment is set. That's why I regretted not knowing it.
Alex
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-forum/9de4a6e0add8444ab699e5026121adf7%40bestweb.net.
Alexandre Rademaker
John F Sowa
JFS:"To Alex: There is no need for you (or anybody else) to lean Python. With the DOL standard, any syntax that conforms to the ISO standard for Common Logic can be automatically translated to and from any syntax that can express FOL or many subsets and supersets of FOL. That includes OWL, Turtle, UML, and even TPTP (Thousands of Problems for Theorem Provers)."
The situation is just the opposite. Formalization of a unit of knowledge (in this case, two theorems) can be placed in the framework of the theory (exactly this one!) in any language. The main thing is that there are enthusiasts who undertake to formalize this particular theory in this particular formal language. And whether it will be a language from the DOL family or Python is the choice of enthusiasts.
The beauty of formalizing a unit of knowledge is that they are usually small (definitions can be several sentences long), of course, except for proofs that can take up terabytes (but in this case it's initially formal). The main thing is that the new unit is consistent with those already in the framework. This structure of the framework of the theory is known but not simple........
Kingsley Idehen
Hi John, Ravi, and other interested parties,
Question: Is there an easy to use tool for generating ontologies that does not require programming language knowledge?
Yes, for example ChatGPT (and similar LLM-based tools).
Prompt:
Generate an Ontology in RDF from the following using terms from
Schema.org, or OWL, RDFS, etc.
Example: https://chatgpt.com/share/670d580f-bdc8-8011-b86c-6451c75d9fcc
-- 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
John F Sowa
Hi John, Ravi, and other interested parties,
Yes, for example ChatGPT (and similar LLM-based tools).
Prompt:
Generate an Ontology in RDF from the following using terms from Schema.org, or OWL, RDFS, etc.
Example: https://chatgpt.com/share/670d580f-bdc8-8011-b86c-6451c75d9fcc
Regards,
Kingsley Idehen
Kingsley Idehen
Hi John,
Kingsley,
I agree that LLMs can be a very good aid to generating ontologies and many other kinds of structures. But by themselves, they often generate false or even hallucinogenic stuff.
Of course! Their output must always be checked. My rule of thumb is: never trust, always verify. That said, they provide immense value in handling grunt work, like generating initial drafts of ontologies based on operator instructions, as demonstrated in the ChatGPT session link I shared.
That's why I liked your multi-step method in an earlier note. It required repeated human evaluation at various stages.
Always! I demonstrate that in ontology generation example I shared.
That is what our Permion.ai work does: use LLMs to generate a hypothesis by abduction and follow up with symbolic methods for testing or evalating to weed out the dubious or even hallucinogenic stuff. Those symbolic methods can be "Ask a human".
For anything more than a simple translation from one notation to another, LLMs by themselves cannot be trusted. Something or someone must always do the testing or evaluation.
They absolutely can’t be trusted blindly, period. As you know, the core issue with LLMs is the age-old battle of marketing hype versus actual deliverable value. Personally, I’ve always viewed the pursuit of AI without human-in-the-loop checkpoints (no matter what clever term marketers invent) as both dangerous and fundamentally flawed.
Kingsley
John
From: "Kingsley Idehen' via ontolog-forum" <ontolo...@googlegroups.com>
Hi John, Ravi, and other interested parties,
Question: Is there an easy to use tool for generating ontologies that does not require programming language knowledge?Yes, for example ChatGPT (and similar LLM-based tools).
Prompt:
Generate an Ontology in RDF from the following using terms from Schema.org, or OWL, RDFS, etc.
Example: https://chatgpt.com/share/670d580f-bdc8-8011-b86c-6451c75d9fcc
Regards,
Kingsley Idehen
--
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/f674b067f6cb4b0ea92043cae3584691%40bestweb.net.
Alex Shkotin
Alexandre,
Thank you for the valuable references. Give me time to get in. Just short remarks to align positions.
(I) Any syntactic structure is welcome as long as we have a processor to create it. The next step is about how fine it is to work with this structure and what is a targeted structure. For example for Programming languages we have non-trivial semantics (static) and pragmatic (execution).
ERS is great!
The topic is that we need to program on attributed trees here.
(II)About https://aclanthology.org/2023.icnlsp-1.19/ let me read it later. And isn't it nice to know that English sentences themselves are HOL? Rhetorical question.
My modest experience is that correct formalization is possible only using formalized theory. And even in this case translation of NL-jargonisms would be manual. But you know more.
(III) Graph theory is just an example of the simplest structure (carrier and binary relation on it) and simplest theory (2 axioms) to show how to keep theory framework and task solving framework.
If you have any reference for Mechanics especially Static please let me know.
The main idea is to find informal axiomatic theory (for ex. Hilbert's Geometry) and formalize it by putting into framework and formal ontology.
But for natural science.
Alex
--
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/9C6B701A-3E81-4B13-AB30-444D809EDDD3%40gmail.com.
alex.shkotin
John,
The theory framework and task framework are proposed to be global: one for all and crowdsourced. Having a hypothesis in the former or a task without solution in the latter, anybody around the World can propose her solution. It would be checked by algorithms and, if the answer would be OK, added to the framework. This is how science and technology should concentrate their knowledge on the Internet era.
Any R&D community from Wolfram Foundation to the lab of enthusiasts can start a framework. Welcome.
And after some time OMG or ISO will release a standard ⚗️
Alex
John F Sowa
alex.shkotin
John,
I had three proposals:
-RFC theory framework,
-RFC task framework and
-Summit 2025 theme. Working title: formalizable and non-formalizable in our formal ontologies. What scientific and engineering knowledge do our ontologies rely on?
We had a summit: ontologies help scientists, and here it is the other way around, scientists help ontologists.
By the way, a very short title for the Summit could be: Theories and Ontologies.
It is clear that none of these proposals will kill science.
On the contrary, the concentration of knowledge will lead to its verification and easier finding and use.
And also to a more systematic development of science and technology.
Please clarify which of my three proposals will lead to the death of science.
Regarding frameworks, I want to emphasize:
Both frameworks are about knowledge concentration, not formalization. But frameworks are a good place to keep all formalizations in one place.
The specific terms "vagueness", "error bounds" are best considered within the framework of a particular theory and technology. The same goes for "precision".
Alex
Polovina, Simon (BTE)
Hi all.
Another commercial product that claims to combine knowledge graphs with LLM. There’s a free version: https://www.ontotext.com/
They were a partner on an EU-funded project I was a leader of 10 years ago: https://cordis.europa.eu/project/id/257403/reporting
I was impressed by them then. May interest.
Simon
John F Sowa
John F Sowa
Sent: 10/18/24 1:48 PM
To: ontolog...@googlegroups.com
Cc: ontolog-forum <ontolo...@googlegroups.com>, CG <c...@lists.iccs-conference.org>
Subject: Re: [ontolog-trustee] Trying to develop a proper useful topic for the 2025 summit
Kingsley Idehen
Hi Ravi,
Still, is there an easy to use tool for generating ontologies that is not requiring programming language knowledge?Thanks.Ravi(Dr. Ravi Sharma, Ph.D. USA)NASA Apollo Achievement AwardFormer Scientific Secretary iSRO HQOntolog Board of TrusteesParticle and Space PhysicsSenior Enterprise Architect
Yes, for example ChatGPT (and similar LLM-based tools).
Prompt:
Generate an Ontology in RDF from the following using terms from
Schema.org, or OWL, RDFS, etc.
Example:
https://chatgpt.com/share/670d580f-bdc8-8011-b86c-6451c75d9fcc
Nadin, Mihai
Dear and respected Kingsley Idehen,
Dear and respected Ravi Sharma,
A not well-formulated question (RS) leads to an answer not better defined than the question—the problem is with
following using terms from Schema.org, or OWL, RDFS, etc.
HOW DO YOU DEFINE ONTOLOGY? Through the tolls currently in use? If so, this is pretty much like thinking in circles.
Neither the question nor the answer to it—both superb—provide the OPEN ENDED understanding of what the ontology task is. Ttranslating siblinghood into computerese via the tool currently deployed is only making the task easier to perform. BUT: leaves the definition of ontology and thus the need to evaluate the outcome open.
Again: impressed. I tried myself. The LLM model based tool are automating what we used to do via programming. Is the LLM model automated programming? Because it is NOT a better understanding of what ontology engineers are doing. ONTOLOGY is fundamentally understanding. Since algorithmic computation cannot, by their condition, understand, ontology engineers explain to them what things are. We give them an actionable dictionary.
Mihai Nadin
--
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/3027e191-3781-4051-9619-2fefe0448c5e%40openlinksw.com.
Alex Shkotin
With John's points as background I suggest that the way to frame a workable summit topic would be to explore the current and likely limits to useful formalization.
----
You received this message because you are subscribed to the Google Groups "ontolog-trustee" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-trust...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-trustee/aa5b81b46277438c865c5733ac7e60c1%40bestweb.net.
You received this message because you are subscribed to the Google Groups "ontolog-trustee" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-trust...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-trustee/CAMhe4f3b%2Bqhv5bGvJUZ2Zf%2BBBaGCGn42TWCLXjseq36yRqzjUQ%40mail.gmail.com.
Polovina, Simon (BTE)
That’s most interesting, John. Thanks! Simon
Gary Berg-Cross
--
You received this message because you are subscribed to the Google Groups "ontolog-trustee" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-trust...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-trustee/606f2e394069451fbd99d0205e825c81%40bestweb.net.
Chris Partridge
--
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/03c6fcb9f79f44e6a6d993f1ec251178%40bestweb.net.
Gary Berg-Cross
--
You received this message because you are subscribed to the Google Groups "ontolog-trustee" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-trust...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-trustee/aa5b81b46277438c865c5733ac7e60c1%40bestweb.net.
jsi...@measures.org
On Oct 19, 2024, at 1:34 PM, Gary Berg-Cross <gberg...@gmail.com> wrote:
With John's points as background I suggest that the way to frame a workable summit topic would be to explore the current and likely limits to useful formalization.
On Wed, Oct 16, 2024 at 2:36 PM John F Sowa <so...@bestweb.net> wrote:
Alex,I have been trying in many different ways to explain why your proposal, if accepted, would be the DEATH of science. Fortunately, no expert in any branch of science would accept it. The following slide from https://jfsowa.com/eswc.pdf explains the issues:
Your proposal is a plan for relating discrete models, as represented by the diagram in the center, to formal notations, such as first-order logic or variations.
By itself that is a good idea. But it ignores the much more difficult left side of the diagram. Physics is the most fundamental of the sciences. Physicists do NOT use formal logic to express their theories. They use many dimensional differential equations. Those theories represent a CONTINUOUS universe and everything in it.As I have been trying to explain, vagueness in natural language is not bad. It's ESSENTIAL in order to relate, explain, and communicate information about the world, our relationships to the world, and our actions in, on, and about the world and everything in it.As engineers say, all those explanations are false in general, but they can be made as precise as required within a level of tolerance that is appropriate for the application.That fact is the reason why systems such as WordNet. Roget's Thesaurus. and ordinary dictionaries are useful for analyzing and reasoning with and about NL information. By being vague, those systems can accommodate the vague statements that occur in all NL documents and communications.Any attempt to map vague statements to FOL or other logic is guaranteed to be false UNLESS the error bounds are explicitly stated and accommodated.If the error bounds are unknown, it's much better to preserve the NL source unchanged. In conclusion, I recommend the eswc.pdf slides. Since they were presented in 2020, they do not mention LLMs. But every sentence derived from NL statements is vague, and the context and information about error bounds is lost.Therefore, no statements derived by LLMs can be trusted unless the error bounds of the source data are known. if the sources are unknown, some system of evaluation is essential. Otherwise, anything LLMs produce must be considered as hypotheses that must be tested and evaluated by some method that uses the above diagram as a prerequisite and guide.JohnFrom: "alex.shkotin" <alex.s...@gmail.com>John,
The theory framework and task framework are proposed to be global: one for all and crowdsourced. Having a hypothesis in the former or a task without solution in the latter, anybody around the World can propose her solution. It would be checked by algorithms and, if the answer would be OK, added to the framework. This is how science and technology should concentrate their knowledge on the Internet era.
Any R&D community from Wolfram Foundation to the lab of enthusiasts can start a framework. Welcome.
And after some time OMG or ISO will release a standard ⚗️
Alex
--
You received this message because you are subscribed to the Google Groups "ontolog-trustee" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-trust...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ontolog-trustee/aa5b81b46277438c865c5733ac7e60c1%40bestweb.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/CAMhe4f3b%2Bqhv5bGvJUZ2Zf%2BBBaGCGn42TWCLXjseq36yRqzjUQ%40mail.gmail.com.