Formalizing Mechanics

[alex.shkotin]

<continuing this>

Gary,

Consider we decide to formalize LL-I sentence by sentence. The first one on page 1(27) is

"One of the fundamental concepts of mechanics is that of a particle."

Formalization may be like this

Declaration particle:(body:TV). --type of "particle" is function from body to true values.

fundamental_concept(particle).

But we need not "fundamental_concept(particle)." in our theory framework as this is a statement about theory, but not from theory.

Second sentence is from theory itself:

"By this we mean a body whose dimensions may be neglected in describing its motion."

⇒

Definition particle(x) : diameter(x)=0.

Where the diameter of a body is the greatest distance between two of its points.

"The possibility of so doing depends, of course, on the conditions of the problem concerned."

This sentence is not from the theory framework, but about a fundamental relationship between a theory and the problems that need to be solved with that theory.

"For example, the planets may be regarded as particles in considering their motion about the Sun, but not in considering their rotation about their axes."

Here we have example of mechanical problems: 

-motion of the planets about the Sun,

-rotation of a planet about its axes.

We should describe separately how to formalize a problem (aka task) and its solution. For ugraphs see Specific tasks of Ugraphia on a particular structure (formulations, solutions, placement in the framework).

So from first passage we get for our formal theory of mechanics:

Declaration particle:(body:TV). 

Definition particle(x) ≝ diameter(x)=0.

And we have here our first definition and its formalization.

Canonical form of definition, i.e. free from author's lyrics is:

A body x is a particle iff diameter of x is 0.

It is important to underscore that this formalization must be in the text of theory together with usual formulas. Like this: 

One of the fundamental concepts of mechanics is that of a particle. The possibility of so doing depends, of course, on the conditions of the problem concerned. For example, the planets may be regarded as particles in considering their motion about the Sun, but not in considering their rotation about their axes.

Declaration particle:(body:TV). Definition particle(x) ≝ diameter(x)=0.

The position of a particle in space is defined by its radius vector r, whose components are its Cartesian co-ordinates x, y, z. 

etc.

In practice formulas should be embedded to the text from theory framework (aka ontology).

The proposal is that we have one theory framework and a lot of presentations of theory: different parts for different public, but with the same formalization from the only one framework for all around the Globe, or organization 🎯

Framework for theory of undirected graphs is here (PDF) Theory framework - knowledge hub message #1 

What do you think?

Alex

[John F Sowa]

Alex,

Physics is the most formal of all the sciences.   The physicists are at the forefront of the most advanced research into the fundamentals of the universe.   The linguists and lexicologists are at the forefront of gathering and relating all the meanings of all the words in all the languages of the world.

Compared to scientists and engineers, ontologists are amateurs.   Compared to the linguists and lexicographers, ontologists are amateurs.   There is absolutely no way that professionals in any of those groups will pay the slightest attention to a bunch of amateurs who try to tell them how to do their job.

Fundamental principle:   As ontologists, we are amateurs compared to the professionals in every branch of the arts and sciences.  But if we do a good job in relating their results to the results of linguists and lexicographers, we can assist in promoting better communication and mappings to and from computer systems.

Bottom line:  Never tell experts in other fields how to do their job.   Our best hope is to help them communicate with each other by means of compatible computer representations.

John

 

---

From: "alex.shkotin" <alex.s...@gmail.com>

[Alex Shkotin]

John,

Formalization of theoretical knowledge hidden in the depths of formal ontologies is a very delicate work. This is work that has its experts. Look at the OBO Foundry projects.

Formalization of theoretical physics, even its section Mechanics, is not needed by physicists themselves. Otherwise, they would have done it long ago.

For well-structured theories, for example, physical ones, we are talking about their construction in the form of axiomatic ones, and then formalization. And of course, this is done together with experts.

Why is this formalization and concentration of theoretical knowledge necessary?

But this is the natural form of existence of knowledge, purified from the subjectivity of authors and lecturers, and the place of its appearance. And our computers and networks allow this.

And our robots need it. I prefer a robot that uses formal theory rather than LLM ⛈️

Alex

вс, 2 мар. 2025 г. в 05:13, 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 visit https://groups.google.com/d/msgid/ontolog-forum/f28c1449dcc54c958be08361d9a2b992%40532a5aec53f54db8b981467face4ef33.

[Alex Shkotin]

IN ADDITION

Any presentation of theory is a literary text with formulas, because it is intended for people.
Formalization of theoretical knowledge itself makes it possible to use it by algorithms in computers, including robots.
I do not claim that a robot should know all theoretical mechanics, but the basics may be useful to it.
However, I claim that all theoretical mechanics can be formalized.

Alex

вс, 2 мар. 2025 г. в 11:20, Alex Shkotin <alex.s...@gmail.com>:

[deddy]

John -

>
> relating all the meanings of all the words in all the languages of the world.
>

But as yet refusing to even admit the existence of the highly unnatural language used in & around software applications?

OAD returns "Royal Canadian Air Force" for RACF!?

______________________
David Eddy

> -------------------------
>
> FROM: "alex.shkotin" <alex.s...@gmail.com>

[John F Sowa]

David,

I'm not sure what point you intended in your very short comment:

In general, there is no limit on what sources lexicographers consider.  I have on occasion attended conferences with them and worked with groups of collaborators.  

But for any particular dictionary, the choice of what words to include depends on the policy of the publisher for whatever edition.  And the publisher needs to make a profit in order to stay in business.   That requires some consideration of the market.

Since a cell phone gives people access to the WWW at any time, that has destroyed the market for traditional dictionaries.  But it hasn't eliminated the need for professional lexicographers.  Unfortunately, professionals are often being replaced by clueless amateurs. 

John

 

---

From: "deddy" <de...@davideddy.com>

John -

>

> relating all the meanings of all the words in all the languages of the world.

>

But as yet refusing to even admit the existence of the highly unnatural language used in & around software applications?

OAD returns "Royal Canadian Air Force" for RACF!?

______________________

David Eddy

> -------Original Message-------

> From: John F Sowa <so...@bestweb.net>

>

[David Eddy]

John -

On Mar 2, 2025, at 2:33 PM, John F Sowa <so...@bestweb.net> wrote:

 what point you intended in your very short comment:

Attempt to state that large slices of “language” used in software applications is far from “natural.”

I seriously doubt if I’ll ever find

M0101

POL-NO

M0760

MENSA-FL

ISSL

LCCIIL01

in a professional dictionary.

A slice of words used in software applications have been made up by programmers … workers who tend to be far removed from the language of the business problem being addressed in the software they are writing & maintaining.

I spoke with the WordNet manager/owner after her talk about how lexicographers decide how/where words fit in WordNet.  She was puzzled by my interest in “words” — like JCL, CICS, IMS — that are NOT in WordNet.

- David

[hpo...@verizon.net]

And then there are all the procedure, function, variable, object, array, etc. names used in software source code that may or may not mean something significant to developers and maintainers. Most of these are unlikely to be found in WordNet or other language references, and even if they happen to do so, are likely to have a significantly different or very application-specific interpretation.

 

Hans

--

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 visit https://groups.google.com/d/msgid/ontolog-forum/9E8D97CA-A683-451B-8E0B-40AEF41432F5%40davideddy.com.

[John F Sowa]

Alex, 

I agree that any ontology implemented on a digital computer cannot be informal.

But science is always a work in progress.  There is no such thing as a finished, perfectly formal scientific ontology that can be guaranteed to be correct about the physical world.

However, it is possible to have a precise formal specification for policies that some company (a bank, for example)  specifies for all the transactions it performs.  That's because all the data and all the transactions are defined to be absolutely precise.

But that level of precision is not possible for physical data that is obtained by any kind of measurements or observations on anything in the universe,

As the engineers say, "All models are wrong, but some are useful."

John

 

---

From: "Alex Shkotin" <alex.s...@gmail.com>
Sent: 3/2/25 3:21 AM
To: ontolo...@googlegroups.com

Subject: Re: [ontolog-forum] Formalizing Mechanics

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORD71%3Dm4eNToyw8u-fa6Y7SNdqK4dkd0fte-bdvp7OJAA%40mail.gmail.com.

[John F Sowa]

David,

I'm not sure if I had replied to this note.  In any case, your point deserves some comment:

DE:  I spoke with the WordNet manager/owner after her talk about how lexicographers decide how/where words fit in WordNet.  She was puzzled by my interest in “words” — like JCL, CICS, IMS — that are NOT in WordNet.

Basic point:   Every dictionary has an editorial policy about what terms they cover.  WordNet policy is similar to the policy of typical dictionaries:  they don't include those words.  But dictionaries designed with a different policy would.  It all depends on the editorial policy.

John

 

---

From: "David Eddy" <de...@davideddy.com>

[Alex Shkotin]

John and copy to MG,

What a pity we do not have slides from M. Gruninger talk here https://ontologforum.com/index.php/ConferenceCall_2025_02_05

Now let's reduce Hilbert-VI to just mechanics. Then we get "Mathematical treatment of the axioms of mechanics: The investigations on the foundations of geometry suggest the problem: To treat in the same manner, by means of axioms, those physical sciences in which mathematics plays an important part."

One way to get this is to formalize the text of informal theory sentence by sentence. Of course only those sentences which are from theory, not about theory.

The subtleness of this process is fixed here https://www.linkedin.com/feed/update/urn:li:activity:7302268310920851456/

And I hope to formalize later the passage #2 🏋️

If we take any formal ontology from for example OBO Foundry, every formula there must have informal form and reference to the text of informal theory presentation, as a justification.

Every good theory is applicable, but by those who know how to apply it properly.

We formalize theories to apply them algorithmically to solve formalized problems. 👏

We have a lot of math theories formalized in Isabelle, Coq, HOL4 etc.

My micro impact for theory of undirected graphs is here (PDF) Theory framework - knowledge hub message #1.

And for application of this theory to task (problem) solving is here Specific tasks of Ugraphia on a particular structure (formulations, solutions, placement in the framework)

But of course, Statics is much more interesting to axiomatize. 

Alex

чт, 6 мар. 2025 г. в 06:02, John F Sowa <so...@bestweb.net>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/ad1a2b69da0f46df8bb7ff190f174d69%4062c8ab776b3145b492c5332090bc6795.

[Kingsley Idehen]

Hi David,

Today, LLMs help handle these kinds of issues -- especially if they have Web-lookup capability (referred to as DeepResearch).

Here's how Grok handles a quest to decipher the terms you presented.

https://x.com/i/grok/share/DABcFHlLqNjuZaP3k1nbETS5M

-- 
Regards,

Kingsley Idehen	      
Founder & CEO 
OpenLink Software   
Home Page: http://www.openlinksw.com
Community Support: https://community.openlinksw.com

Social Media:
LinkedIn: http://www.linkedin.com/in/kidehen
Twitter : https://twitter.com/kidehen

[Alexandre Rademaker]

John,

You are probably talking about Christianne Fellbaum. She assumed the Princeton Wordnet leadership after George Miller. I am part of the Global Wordnet Association's board and the Portuguese Wordnet's primary maintainer. I also collaborate with https://en-word.net/, a fork from the mother of all wordnets, the Princeton Wordnet.

Indeed, the examples you gave are pretty radical. Are the JCL, CICS, and IMS abbreviations or acronyms? Your point is correct, and in the case of Wordnet, we have many terms related to baseball (much more than any other sport) and birds just because Miller liked these subjects. As you said, editorial policy and/or commercial arguments are used in the decision about coverage for dictionaries.

Best,
Alexandre

[John F Sowa]

Alexandre,

I have been working on aspects of computational linguistics for years, and the problems of dealing with acronyms, abbreviations, and technical vocabulary of any kind has always been a complex issue.  Organic chemistry, for example, has a systematic method for generating millions of character strings that represent organic molecules.  

In my note below, "DE" marks a quotation by David Eddy, who cited the strings M0101, POL-NO, M0760, MENSA-FL, ISSL, LCCIIL01.

Any of those strings may occur in a sentence, but almost always in the same positions as proper names.  Therefore, any occurrences can be handled fairly well by treating them as a kind of names.   In Chinese, however, names create serious difficulties because almost any Chinese characters can be used in proper names.   

In our old VivoMind system and our new Permion version, we have had to deal with all those issues.  We also have to deal with text that switches between languages (natural and/or artificial) in the middle of a sentence.  They create additional difficulties, which both systems have been able to deal with by using a parsing method that can accommodate language switching.

As for WordNet, that is one of multiple resources that the VivoMind and Permion systems use.

John

 

---

From: "Alexandre Rademaker" <arade...@gmail.com

[John F Sowa]

David and Kingsley,

I just wrote a reply to Alexandre.  See that note for a comment about what VivoMind and Permion do.

But that response from Grok is terrible. It shows why such systems generate hallucinations.

What Permion does is to treat such terms as a kind of proper name when parsing the sentence.  But it also adds the names to a list of unresolved references, which can later by linked to other occurrences of those names in the same or other texts.

For organic molecules, VivoMind had an excellent method for dealing with them.  See https://jfsowa.com/talks/cogmem.pdf .

The  first example in the last section of that talk shows how VivoMind outperformed all other competitors in analyzing texts about organic chemistry. 

By the way, Arun Majumdar had been working for a PhD in organic chemistry, when he almost died when his experiment blew up.  That's when he decided it was time to switch to computer science.

John

 

---

From: "Kingsley Idehen' via ontolog-forum" <ontolo...@googlegroups.com>

Hi David,

[Kingsley Idehen]

Hi John,

On 3/6/25 6:31 PM, John F Sowa wrote:

David and Kingsley,

I just wrote a reply to Alexandre.  See that note for a comment about what VivoMind and Permion do.

But that response from Grok is terrible. It shows why such systems generate hallucinations.

What Permion does is to treat such terms as a kind of proper name when parsing the sentence.  But it also adds the names to a list of unresolved references, which can later by linked to other occurrences of those names in the same or other texts.

For organic molecules, VivoMind had an excellent method for dealing with them.  See https://jfsowa.com/talks/cogmem.pdf .

The  first example in the last section of that talk shows how VivoMind outperformed all other competitors in analyzing texts about organic chemistry. 

By the way, Arun Majumdar had been working for a PhD in organic chemistry, when he almost died when his experiment blew up.  That's when he decided it was time to switch to computer science.

John

 

The intent of my response wasn’t to suggest that an LLM would produce a perfect response. Rather, it was to highlight that David’s quest is inherently fuzzy—a challenge well-suited to tools like LLMs, especially when equipped with Web search and research capability.

For example, the rough draft from Grok serves as an early-stage conversation starter, ultimately leading to the construction of a taxonomy or ontology that can be deployed using a variety of notations.

Kingsley

--

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 visit https://groups.google.com/d/msgid/ontolog-forum/f80e9338fdb0498796cbd0def06ac0f7%4091cac3c6f93f4e478b11a5e86bd49d4a.

[David Whitten]

At least some of them are on Wiktionary.

JCL -- JCL - Wiktionary, the free dictionary https://en.wiktionary.org/wiki/JCL

IMS -- IMS - Wiktionary, the free dictionary  https://en.wiktionary.org/wiki/IMS

Dave Whitten

713-870-3834

[David Whitten]

Perhaps I'm missing something, but isn't Michael Gruninger's audio here?

ontologforum.s3.us-east-1.amazonaws.com/OntologySummit2025/Track-1/The+Heirs+of+Hilbert's+Sixth+Problem--MichaelGruninger_20250205.mp4

Dave Whitten

713-870-3834

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORXANt%2BW5Y%3DFTxv7N1L8BUipikCGTGeRnVv4GjVo7XBsQ%40mail.gmail.com.

[David Eddy]

Kingsley -

On Mar 6, 2025, at 7:21 PM, 'Kingsley Idehen' via ontolog-forum <ontolo...@googlegroups.com> wrote:

David’s quest is inherently fuzzy—a challenge well-suited to tools like LLMs, especially when equipped with Web search and research capability. 

I’ll have to put that into my patter… “Is your nightly cycle web enabled & available to LLM process?”

I’m thinking most likely not.

We’ll see.

BTW… my quest is absolutely NOT “fuzzy.”

For folks working behind corporate firewalls, precision & completeness of searchs is extremely important — not related to Google search — where names (labels?) like LCCIIL01 have very explicit meanings.

the rough draft from Grok 

You would expose corporate JCL to Grok!?

- David

[Alex Shkotin]

Dave,

Yes, and not only audio but video too. And usually it is possible to get slides, like pdf, ppt, you know.

For example here https://ontologforum.com/index.php/ConferenceCall_2025_02_26 we have slides.

And here https://ontologforum.com/index.php/ConferenceCall_2025_02_05 we have not.

Alex

пт, 7 мар. 2025 г. в 04:00, David Whitten <whi...@worldvista.org>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAH8N84yKOEUeXZbJGndRx_0rJRtrcOgX-MrUcW48DDMQ4osPmg%40mail.gmail.com.

[David Whitten]

Thank you for clarifying 

To unsubscribe from this group and stop receiving emails from it, send an email to ontolog-forum+unsubscribe@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/f28c1449dcc54c958be08361d9a2b992%40532a5aec53f54db8b981467face4ef33.

--

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-forum+unsubscribe@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORD71%3Dm4eNToyw8u-fa6Y7SNdqK4dkd0fte-bdvp7OJAA%40mail.gmail.com.

--
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-forum+unsubscribe@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/ad1a2b69da0f46df8bb7ff190f174d69%4062c8ab776b3145b492c5332090bc6795.

--
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-forum+unsubscribe@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxRORXANt%2BW5Y%3DFTxv7N1L8BUipikCGTGeRnVv4GjVo7XBsQ%40mail.gmail.com.

--
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-forum+unsubscribe@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAH8N84yKOEUeXZbJGndRx_0rJRtrcOgX-MrUcW48DDMQ4osPmg%40mail.gmail.com.

--

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-forum+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CAFxxROT%3D%2B1e8i6vqCMRqP4y3DibhKUzkbUyug1gEfTy_dV3RrQ%40mail.gmail.com.