Computable Contracts for Insurance: Establishing an Insurance-Specific Controlled Natural Language - InsurLE
Alex Shkotin
Prof. N.E. Fuchs, leader of the Attempto project, gave us a reference to this year's article [1] representing InsurLE - CNL for the Insurance domain of practice. Where we have
"Types in InsurLE impose a hierarchical structure on the universe of discourse. In this hierarchy, concrete objects are situated at the bottom of the hierarchy, and abstract classes appear at higher levels, with subclasses occurring directly below their parent class. This hierarchy of objects and classes can be viewed as part of a domain-specific ontology for insurance contracts49.
49 An ontology is a set of concepts, properties and relationships in a subject area or domain underpinning the vocabulary of a language for that domain."
Of course, the most interesting thing is the kind of knowledge processing available.
Creating a formal theory for Insurance area of practice may be next.
Alex
John F Sowa
Sent: 7/19/25 2:16 AM
Bill Nadal
Hi John,
I’m curious - did you ever work with IBM’s Insurance Application Architecture (IAA)?
The IAA model was a generic untyped insurance model culled from many of IBM's P&C insurance engagements in the '90s
Back in 2001, I was part of the Beacon Claims Project at Fireman’s Fund Insurance Company (FFIC), where we used the untyped Smalltalk-based IAA model and typed it for Java code generation. IBM actually accepted our updated version as a Type 2 deliverable.
We treated the IAA model as canonical, extending from it rather than modifying its core. Any changes we proposed were coordinated directly with IBM.
Our work on Beacon was later referenced in a 2004 Computerworld article on Model-Driven Architecture (MDA) projects, highlighting how FFIC used IAA for component generation:
At the time, many saw IAA as the foundation of an emerging insurance business ontology, and it was often referenced alongside the ACORD and OMG models.
That was quite a while ago, and I’m not sure whether more recent efforts like the ACORD standards or ISO 20022 have since taken precedence in defining canonical insurance models in the P&C subgroup.
Best, Bill
https://www.computerworld.com/article/1701997/blueprint-for-code-automation.html
--
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/33979d80c4f5459c95e4d06a477b9866%408dfdd6a66a3f4fdebb414f173d95f4f0.
Alex Shkotin
John,
I am sending a copy to Prof. Robert Kowalski for possible feedback.
Any formal ontology keeps formal theory and a model of this theory. In terminology of Description Logics (OWL2) formal theory is T-box, and model is A-box.
If somebody is using InsurLE or Common Logic the situation will be the same, but with different terminology.
What is funny with the OWL2\DL approach is that they keep all terms (for classes, and properties) as primary. And all T-box formulas as axioms. They actually call them "axioms".
Step forward to the formal theory is to give definition for most terms.
And you are right: applicability of a theory may be very narrow, for example just an organization, or even family. Where we have our own special terms and definitions for objects and processes.
So, definitions in the Insurance area is the first step to theory.
Alex
John F Sowa
John F Sowa
Sent: 7/21/25 12:06 AM
Alex Shkotin
John, I am sending a copy to Prof. Edward Zalta just for a chance to get his point
Any philosophical doctrine is a general-purpose ontology. We may choose any to formalize.
We need just one or another enthusiast for this exciting work.
A great example is Edward Zalta's formalization of metaphysics Principia Logico-Metaphysica (Draft/Excerpt).
Interconnection of domain specific theories and philosophical doctrine for me lies in Phenomenology of Matter (PhoM). Which maybe is a part of phanerology.
For us, the main theme of PhoM is the geometry of luminous surfaces of different colors in different places. Just look around you to start applying this general-purpose theory.
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 visit https://groups.google.com/d/msgid/ontolog-forum/b8f49ebc3ff143388b25156af169921e%40551ba8aeac044aeab5bc11a74f84ea83.
Bill Nadal
Perhaps we have to decode the origins of the "Big Bang" to establish the start of a universal ontology of everything. We have a hint where to start, "In the beginning was the Word". ;-)
Best, Bill
--
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/c18b018aabe5457bbdd8339c79c0e508%40a0ac0b5475e54bec9532a60481aebb54.
John F Sowa
Sent: 7/22/25 8:18 PM
To: ontolo...@googlegroups.com
Cc: so...@bestweb.ne
Subject: Re: [ontolog-forum] Computable Contracts for Insurance: Establishing an Insurance-Specific Controlled Natural Language - InsurLE
John F Sowa
Sent: 7/22/25 4:42 AM
To: ontolo...@googlegroups.com
Cc: "Norbert E. Fuchs" <fu...@ifi.uzh.ch>, r...@doc.ic.ac.uk, Edward Zalta <za...@mally.stanford.edu>
Subject: Re: [ontolog-forum] Computable Contracts for Insurance: Establishing an Insurance-Specific Controlled Natural Language - InsurLE
Alex Shkotin
Dear Ed, I see your letter is not in our forum. but I hope it will be in my reply,
Let me answer in the first approximation. Here we formalize various knowledge and formalize them as formal ontologies. I used "formal" again to emphasize their difference from informal ontologies which they also say someone saw somewhere.
May I note right away that the whole charm of formalization is that we know the rules of inference for formal theories, i.e. we can assign algorithms to one of the essential knowledge processing. We also know how to build mathematical models of these theories that will have some properties the same as part of reality. As a result, we can request such a model and not reality.
Formalization is just a mathematical recording of knowledge.
Some people think that some knowledge is lost during the transition to formalization. This is true, but what is lost is not essential for the task at hand.
After all, we apply theoretical knowledge to solve problems.
You have geometric objects and relations. But this is the first step to practical problems.
Formalization of Metaphysics is very cool. Especially since you have built an axiomatic theory.
How do you see its connection with physics?
In addition, your theory can be very useful for our Top-Level Ontologies [1]. If you have time and desire to look at them.
What are the applications of your theory?
It is important for me to show our community that there is a formal theory of metaphysics. And Hilbert's VI problem has not yet been solved. M. Gruninger told us about the state and prospects at the last summit.
Your distinction between pretheoretical and "in the theory" knowledge is very important for our ontologies, since we can say that they are all pretheoretical😀
Best regards,
Alex
[1] Please read this Gemini overview https://g.co/gemini/share/42a150a1b316
or this "The Basic Formal Ontology (BFO) is a small, upper-level ontology that is designed for use in supporting information retrieval, analysis and integration in scientific and other domains. BFO is a genuine upper ontology. Thus it does not contain physical, chemical, biological or other terms which would properly fall within the coverage domains of the special sciences."
https://github.com/BFO-ontology/BFO
The level of abstraction is metaphysical.
Dear Alex,
Thanks for looping me into your discussion and for referencing my unpublished monograph, in which I’ve been compiling theorems proved in object theory over the past 40 years. I looked up your discussion on groups.google.com and I see that your last message seems to be a reaction to the remark by John Sowa, who wrote:
> I strongly support projects to develop special-purpose ontologies for various industries. And I'm sure that the one you describe is good for its purpose. But I had seen so many projects, that I am extremely skeptical about any attempt to develop a universal ontology of everything.
Given what he says, I doubt John will find that the system developed in Principia Logico-Metaphysica is a universal ontology of everything. Indeed, that wasn’t what it was designed to be, though it was designed to start with the highest level ontological categories of objects and relations.
If you do look at that monograph, I would characterize it as an attempt to systematize and analyze the abstract objects, such as mathematical objects, that are presupposed in the natural sciences and in the "a priori" sciences (logic, linguistics, etc.). I’m not a Pythagorean and so I don’t think that mathematical objects are fundamental elements of the universe. So to account for the meaningfulness and content of mathematical language, we need a philosophical analysis of that language. That is one application of object theory. It might come as a surprise just how much mathematics can be derived from a system which doesn’t assume any mathematics but only logical principles and a few high-level axioms about the two fundamental categories of objects and relations (I use second-order quantified modal logic with just one extra mode of predication for the base system, but then re-express the theory using relational type theory).
In general, goal is to use object theory to *define* abstract objects that others postulate, and *derive* the governing principles that are asserted of them. The List of Important Theorems and the Table of Contents will tell you what I mean by this.
But I haven’t attempted to work on any applied ontologies of the kind being discussed in this thread on ontolog-forum. To that extent, I don’t have much to offer.
In any case, thanks for pointing out my work.
All the best,
Yours,
Ed
> On Jul 22, 2025, at 1:41 AM, Alex Shkotin <alex.s...@gmail.com> wrote:
>
> John, I am sending a copy to Prof. Edward Zalta just for a chance to get his point
>
> Any philosophical doctrine is a general-purpose ontology. We may choose any to formalize.
> We need just one or another enthusiast for this exciting work.
> A great example is Edward Zalta's formalization of metaphysics Principia Logico-Metaphysica (Draft/Excerpt).
> Interconnection of domain specific theories and philosophical doctrine for me lies in Phenomenology of Matter (PhoM). Which maybe is a part of phanerology.
> For us, the main theme of PhoM is the geometry of luminous surfaces of different colors in different places. Just look around you to start applying this general-purpose theory.
>
> Alex
>
> пн, 21 июл. 2025 г. в 19:53, John F Sowa <so...@bestweb.net>:
> Alex,
>
> I've known Robert Kowalski for many years, and he is an expert in developing formal theories for various purposes.
>
> But the point I keep stating is that independently developed special-purpose theories make special-case assumptions (axioms) that are almost always incompatible (inconsistent) with the special cases for other purposes.
>
> For these reasons, a collection of multiple special-case theories will NOT give you a general-purpose ontology.
>
> John
>
Alex Shkotin
John,
This is the difference. We are not creating knowledge. We are systematizing and formalizing existing ones. It is a requirement to do this with experts. Yes, there is a point that the same knowledge about reality may be formalized into different theories. But this is a problem inside this approach, not before.
Formalization makes knowledge concentration millions of times better than LLM. We have not too many theories, maybe 100 000.
Just to feel how metaphysics can be formalized, have a look at Principia Logico-Metaphysica (Draft/Excerpt). Where we have on p.254: "Now that we have a precisely-specified philosophical language that allows to
express claims using primitive and defined notions, we next assert the fundamental
axioms of our theory in terms of these notions. We may group these
axioms as follows:
• Axioms for negations and conditionals
• Axioms for universal quantification and logical existence
• Axioms for the substitution of identicals
• Axioms for actuality
• Axioms for necessity
• Axioms for necessity and actuality
• Axioms for definite descriptions
• Axioms for relations
• Axioms for encoding
The statement of certain axiom groups require preliminary definitions.
"
Alex
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/bb4425c6c7ea43c798fd03937979e67a%402d96ce56d68745b9a6a029af66c8abad.
John F Sowa
Sent: 7/23/25 9:03 AM
Alex Shkotin
John,
Let me point out that this particular group https://groups.google.com/g/ontolog-forum is for exchange of ontological ideas. For the committee they have another google group.
Yes I sent my ideas to our community one more time, but I hope our community may be interesting for Norbert, Bob, and Ed.
And I think it's time to stop cc them our discussion.
I hope to present the first version of an axiomatic theory of statics this fall. Sorry for the delay. I myself am surprised at how many subtle nuances must be taken into account when moving from geometric worlds to the static worlds of physics. And the next project will have to axiomatize the laws of motion.
Alex
To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/25d9ff9e87a042b4a0e4d94043a5a732%406c85e20878b54686b801266a078d3fac.
John F Sowa
John,
Let me point out that this particular group https://groups.google.com/g/ontolog-forum is for exchange of ontological ideas. For the committee they have another google group.
Yes I sent my ideas to our community one more time, but I hope our community may be interesting for Norbert, Bob, and Ed.
And I think it's time to stop cc them our discussion.
I hope to present the first version of an axiomatic theory of statics this fall. Sorry for the delay. I myself am surprised at how many subtle nuances must be taken into account when moving from geometric worlds to the static worlds of physics. And the next project will have to axiomatize the laws of motion.
Alex Shkotin
John,
This is an ongoing misunderstanding. I, like the vast majority of formal ontologists, do not create new knowledge. I formalize existing knowledge. A classic example is the formalization of the first paragraph of a textbook on graphs. The report is here (PDF) Theory framework - knowledge hub message #1 and there is a link to the textbook there.
And this is the number one rule of formalization: each formula must have a link to an authoritative text with its formulation in natural language.
Among the books on mechanics, I will mention the fundamental course by Landau and Lifshitz, Theoretical Physics, Volume I, Mechanics.
And again, as with undirected graphs, we are talking about formalizing a tiny part of all theoretical knowledge. Just to see how it looks.
I am sure that you can formalize a piece of knowledge in mechanics. You don't have to be a Nobel laureate for this.
It is important that the axiomatic theory of geometry can be taken from Hilbert. But it will also need to be formalized.
The criterion of good formalization: we have algorithms for solving practical problems based on it. For undirected graphs, the report is here Specific tasks of Ugraphia on a particular structure (formulations, solutions, placement in the framework).
key points: formalization of existing knowledge, axiomatic theory, finite structure.
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 visit https://groups.google.com/d/msgid/ontolog-forum/1c0487fd9eb24c01a468a6abb868b2b4%40437e20c983ed423a8e72b07da422c8e4.
John F Sowa
John,
Alex Shkotin
John,
How many specific theories are there in physics is a separate interesting question for a philosopher of science. How many are there in theoretical mechanics, I will probably find out by the end of the year. This is a small cataloging project that is worth doing.
As a science that could be considered much more "formalized" or formalizable than physics, one can point to mathematics.
But mathematicians are not at all fans of formalizing their theories. Like all experts, they are in the position: everything is clear anyway.
What is the formalization of a mathematical theory is best considered with an example. I have already given links to my work on the formalization of one paragraph from a textbook on graph theory.
But here is an example of a much more complete formalization in a language that allows the construction and verification of proofs [1].
This is an example of the formalization of a mathematical theory.
This is just a special kind of project, but very close to formalization we do in our ontologies.
It's amazing that we have some formalizations for quantum mechanics and none for classical: https://www.isa-afp.org/search/?s=mechanics.
And I completely agree with your "The best that we and our Ontolog colleagues can do is to provide a framework that enables communication and collaboration among the professionals in physics (and other subjects)." But changing "The best that" to "What"🏋️
I have the same idea expressed with a different emphasis: "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."
Alex
[1] https://www.isa-afp.org/entries/Undirected_Graph_Theory.html
This entry presents a general library for undirected graph theory - enabling reasoning on simple graphs and undirected graphs with loops. It primarily is inspired by Noschinski's basic ugraph definition in the Girth Chromatic Entry, however generalises it in a number of ways and significantly expands on the range of basic graph theory definitions formalised.
--
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/7a3ed905d8034500a7c08e93af31fcb9%40f12c0baabbbd4987a107df96ae6715a6.