FOL and Industries

[Alex Shkotin]

Yesterday, after Will Sobel's fascinating talk [0], JFS once again urged everyone to use FOL. Will said (my interpretation) that no one is against it; just provide a suitable tool for practical tasks.

I asked Deepseek about it and received a helpful answer [1].

It's worth looking into the applicability of the mentioned tools to the needs of formal ontologies.

Alex

[0] https://ontologforum.com/index.php/ConferenceCall_2026_04_29 

[1] https://chat.deepseek.com/share/ht7cgofjuq7vo0xxob

Here's the translation of our exchange:

**My question:**

"Are there any applied, non-academic projects where FOL is used for knowledge formalization?"

**Your answer:**

Yes, such projects exist, and first-order logic (FOL) in them is not just theory but a working tool for critically important systems. Its areas of application range from verifying train safety to configuring insurance products.

Here are several striking examples from different industries:

*   **🏭 Industrial Automation Systems**: The **ISO 18629 (PSL)** standard is based on first-order logic and is used for the unambiguous description and integration of manufacturing processes.

*   **🚆 Railway Safety**: The **B-Method** is a formal method actively used in the railway industry to create safety-critical software. It is based on first-order logic and set theory. For automated proof of correctness of such code in the B-Method, the **Zenon** tool is used — an automated theorem prover based on first-order logic.

*   **⚖️ Knowledge Management and Configuration**: The **Logic.Tools** platform helps companies, including an insurance company in France and railway operators in Belgium, to create applications based on semantic web technologies. To describe business logic, which is then directly executed, the **OWL** and **SWRL** languages are used, which are based on first-order logic (description logics).

*   **⚙️ Interactive Configurators**: The **IDP-Z3** engine is used to create configurators for complex products or services. It works with the **FO(.)** (FO-dot) knowledge representation language, which is a direct extension of first-order logic.

These examples clearly demonstrate that FOL is successfully applied for knowledge formalization in the real world. If you are interested in a specific example or industry, I can find more detailed information.

[alex.shkotin]

IN ADDITION

You know I am a fan of HOL, as (PDF) English is a HOL language message #1X

So I asked Deepseek the next question and got a very interesting answer:

Here’s the translation of our latest exchange:

---

**My question:**

"What can be said about the application of HOL? After all, commonly used formal languages have capabilities that go beyond FOL."

**Your answer:**

Your observation that many formal languages in practice go beyond the capabilities of first-order logic (FOL) is absolutely correct. Higher-Order Logic (HOL) is indeed actively used in industry, especially in tasks that demand exceptionally high reliability and where the expressiveness of FOL proves insufficient. Its main advantage is the ability to treat functions as objects, pass them as arguments, and quantify over predicates.

Here are several specific examples of applied use of HOL, demonstrating a wide range of tasks, from cloud computing to finance.

### 🛡️ Formal Verification of Critical Software and Hardware

This is perhaps the most well-known and important area of HOL application in industry. When the cost of an error in software or hardware is unacceptably high, mathematical proof of correctness, often based on HOL, comes to the rescue.

*   **Amazon's Cloud Hypervisor**: One of the most prominent and recent examples is the **AWS Nitro Isolation Engine**. This is a key security component that isolates the data and computations of different customers on a single physical server. For its formal verification, Amazon engineers used the **Isabelle/HOL** proof assistant. This made it possible to create a rigorous mathematical proof that guarantees the functional correctness and reliability of the isolation, ruling out design-level errors. This proof, consisting of 260,000 lines of machine-checkable code, became the world's first for a cloud hypervisor.

*   **Verification of Algorithms at Intel**: Intel has been using interactive theorem provers for many years, in particular **HOL Light**, for the formal verification of floating-point algorithms (division, square root extraction, transcendental functions). This is critically important for ensuring the correctness of computations in processors and preventing notoriously famous errors like the "Pentium FDIV bug".

*   **System Reliability Analysis**: There is also a whole field of applying HOL (for example, using the **HOL4** system) to conduct not just testing, but formal reliability analysis of complex engineering systems. Unlike simulations, which only check a subset of possible states, theorem provers allow for exhaustive analysis of models such as Reliability Block Diagrams and Event Trees.

### ⚙️ Intelligent Industrial Systems

Another direction where HOL is finding increasingly active application is the creation of systems capable of reasoning, configuring, and solving complex tasks.

*   **"Intelligent" Configurator**: The **Imandra** system uses computational higher-order logic (based on a subset of the OCaml language) and is applied to solve tasks with a high degree of complexity. For example, financial giant **Goldman Sachs** has publicly stated that it uses Imandra for designing and auditing its most complex trading algorithms.

*   **Working with Knowledge Graphs**: Systems are being developed that attempt to use the expressiveness of HOL for reasoning over knowledge graphs. An example is **ULKB Logic** — an open-source Python framework that provides an interactive environment for representing common sense and linguistic knowledge using a language similar to HOL Light.

*   **Upper-Level Ontologies**: The standard Suggested Upper Merged Ontology (**SUMO**), which is used for information integration in various systems, is originally described in the **SUO-KIF** language, which is a higher-order logic.

### 🧠 Industrial Automation and "Enterprise 2.0"

*   **EnterpriseWeb**: This company directly uses higher-order logic, types, and functions to create real-time systems that enable enterprise automation and network process management at a new level of flexibility and reliability.

### 🤔 So Why Isn't HOL Used Everywhere?

It is important to understand the cost of such power:

*   **High Complexity**: Working with theorem provers (Isabelle/HOL, HOL Light) requires very high qualifications and is an extremely labor-intensive process.

*   **Computational Complexity**: Proving theorems in higher-order logic is algorithmically much more complex, and automatic decision procedures for it are, in general, impossible.

*   **Niche Application**: Due to these limitations, HOL is not used everywhere but mainly where the risks and cost of an error outweigh the labor costs of formal proof.

Thus, if FOL dominates where there is a need for automated reasoning and a good balance between expressiveness and computational complexity, HOL is the "heavy artillery" deployed when the stakes are at their highest and an impeccable mathematical guarantee of correctness is required — one that cannot be obtained by other means.

If any of these areas or tools particularly interest you, I can provide more detailed information.

четверг, 30 апреля 2026 г. в 11:25:07 UTC+3, Alex Shkotin:

[Jake Waas]

Sorry, for context do you consider acl2 (automatic theorem prover) https://acl2.org/ i.e. https://link.springer.com/book/10.1007/978-1-4757-3188-0 an example of first order logic for reasoning about systems. I still have to catch up on today's but I am especially interested now.

I am very interested in this dicussion. I think I misread you but it is not like higher order logic is better first order logic. More expressive but with different implications.

--
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/a22fefc1-f89e-4b57-ac67-b32e4badba39n%40googlegroups.com.

[Jake Waas]

I guess I should point out for context that acl2 has support for limited second order logic under the tameness restrictions you can imagine. I guess higher order logic here mainly means third order order a less tame second order logic. Sorry I again I have not watched the summit yet.

Erik Sandewall, whose KRF I unbitrotted did write that he thought you did not need to have formal proofs to work in an ontological way, but my own feeling is in support of first order logic and automatic theorem proving.

I saw the mathematician Vassil Nikolov recently write that in the context of LLM generated code, writing first order logic and hence automatic proof amenable programs seemed like a safe place to choose now more than ever.

[Alex Shkotin]

Hi Jake,

I just mentioned that JFS stands for FOL and I am a fan of HOL.

I don't know acl2. Here https://chat.deepseek.com/share/blq9lxutzhaebo47zc is Ds point.

The main topic is usage of different powerful formal languages for formal ontology tasks and processes i.e. for formal knowledge representation and processing.

But just to begin classification: any language more syntactically powerful than FOL is HOL for me.

See an example from [1]. So OWL2DS is a HOL translatable to FOL.

Alex

[1] https://www.researchgate.net/publication/336363623_OWL_2_Functional_Style_operators_from_HOL_point_of_view 

HOL features

Here for convenience we summarize all features we need to define OWL 2 operators in HOL.

sorts. We need 2 sorts embedded in the HOL-language:

d - literals of the form LV^^DT [DS], for example "1"^^xsd:integer. Sort d is populated by literals.

Nat - natural numbers.

We declare sort o to keep OWL2-objects:

Declaration o sort.

operators - functions from/to predicates and functions.

predicators - predicate from predicates and functions. 

definitions for constants, functions, predicates. 

# - quantifier for quantity.

чт, 30 апр. 2026 г. в 12:09, Jake Waas <ja...@waas.nz>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CANTuYBu4_HCtpehhQOKhg_S-jW3y_qYD87PKxwgoMTmJw%3DhqqA%40mail.gmail.com.

[Alex Shkotin]

The main task is to properly represent our knowledge in formal language and get useful knowledge processing.

Our initial knowledge is usually in natural language with some math inclusions.

Today in OWL2 ontologies we have that some knowledge can't be expressed in OWL2 but in FOL++ it's possible and they put these formulas in annotations.

An interesting question is what kind of KG-processing we have for OWL2 and how to organize the same or broder in other formal languages.

From Deepseek we have that formal languages are used for very heavy tasks to compare with formal ontologies.

Alex

чт, 30 апр. 2026 г. в 12:29, Jake Waas <ja...@waas.nz>:

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

[John F Sowa]

Jake and Alex,

I strongly agree that some versions of HOL are extremely valuable.  In the Ontology Summit discussion yesterday, I said that FOL is vastly superior to OWL and vastly SIMPLER to state and translate to and from natural languages.   That was important to move the discussion away from using OWL for new applications.  But the old applications will continue to be used for many years.  We must develop methods for supporting both

But I certainly agree that general reasoning systems must also support higher-order methods that go beyond FOL.  The ISO standard for Commmon Logic (CL) does indeed do that.  I was working on the design committee for CL, and I have been working with colleagues to develop technology to support CL and its applications to higher-level reasoning methods.

However, I certainly admit that there is a huge number of applications that are still based on OWL.  They are important for many reasons, and they will not be replaced for many years.  Therefore, we must develop tools and methodologies that can continue to use the old software while MIGRATING to more general and more expressive methods.

Fortunately, the new AI methods based on LLM technology can support mappings of logics of any kind  to and from natural languages (English, Chinese, Russian, French, German, etc,).  They enable users to speak their native languages when mapping and updating old representations to new versions in more general and expressive systems.

These  methods enable the old technology to be used indefinitely in conjunction with new technology based on more general logics such as CL.  The old systems can remain in use to support the old applications while the new logics can support extensions that interact with them and go beyond them.  And users can talk with both systems in their familiar natural languages.

Tim Berners-Lee had an excellent proposal in 2000 for using HOL for the Semantic Web.  Unfortunately, Tim's original design was hijacked by certain people who destroyed his vision by watering it down to OWL.  Common Logic is essentially Tim's original vision.   I presented a summary of the issues at the European Semantic Web Conference in 2020:  https://jfsowa.com/talks/eswc.pdf .

There are 64 slides in this file, but I only had time to present the first 32 at the conference.  Those 32 slides are sufficient to show the importance of Common Logic and the CLIP notation.  The remaining 32 get into other issues that are also significant, but they go beyond the basics.  The 64th slide has more references for further background.

John

PS:  I hate to brag.  But that talk got the best presentation award for the conference.

 

---

From: "Jake Waas" <ja...@waas.nz>

[Jans Aasman]

Inspired by some discussions here I have implemented an experimental Common Logic / CLIF layer for AllegroGraph, using a combination of Prolog and Lisp. I am now looking for more substantial test cases to stress-test the implementation.

To be clear, we already have enough large Prolog programs, and we also have access to large ontologies that require only description-logic-style reasoning. What I am looking for is different: larger Common Logic / CLIF test cases that go beyond what can be handled naturally by Prolog alone or by OWL/DL-style reasoning alone.

LLMs have been surprisingly useful for generating small CLIF examples, especially examples involving quantification, implications, and rule interactions that exceed the expressivity of description logic or straightforward Prolog execution. However, most generated or publicly available examples are still quite small.

I need larger Common Logic or CLIF theories: examples with many interacting axioms, rules, quantifiers, implications, constraints, and modeling patterns that are awkward or impossible to express cleanly in OWL/DL or plain Prolog.

Does anyone have access to one of those?

thanks, Jans

--
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/CAFxxROQi61hdp%2BFAR0iBr-iVLjL4_UR8Njf9hdtkiDnnHqOpMg%40mail.gmail.com.

[Alex Shkotin]

Hi Jans,

I'd be interested in learning more about your project.

What theories are you interested in?

On the one hand, FOL, CL sometimes appears in OWL2 ontology annotations. You could try searching OWL2 ontology repositories.

On the other hand, provers (Isabelle, Rocq, Lean4, etc.) have many mathematical theories, and sometimes even physical ones.

Take Geocoq, for example.

What kind of knowledge processing can be done in your CL implementation?

For example, compared to the capabilities provided by the reasoner in Protege?

Do you have an OWL2 to CL converter?

Do you have examples of the expressive power of CL?

But the main question is: what kind of knowledge processing can be performed by formalizing it in CL?

Alex

P.S. I asked Deepseek: `Jans wrote "I have implemented an experimental Common Logic / CLIF layer for AllegroGraph, using a combination of Prolog and Lisp. I am now looking for more substantial test cases to stress-test the implementation." can you help him?`

The answer may be interesting https://chat.deepseek.com/share/qpfcq1ex8cdj3maehg

пт, 1 мая 2026 г. в 21:08, 'Jans Aasman' via ontolog-forum <ontolo...@googlegroups.com>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CABd59doT2RQQ%2BBLN01imy6eUK9v__X-Lke57pB%2BcvqJNszyDpw%40mail.gmail.com.

[Alex Shkotin]

Jans,

You can find interesting definitions for formalization in these two frameworks: graph framework, geometry framework.

And if you provide a formalization in CL, I'd be happy to add a line, designating the language, for example, as cl.

Here's an example of multilingua.

I21 axiom

rus	Пусть A, B - точки. Если A и B различны то существует единственная прямая которая соединяет A с B.
eng	Let A and B be points. If A and B are distinct, then there exists a unique straight line that connects A to B.
yfl	∀p1,p2:Po p1≠p2 → (∃1l:SL connects(l p1 p2)).
coq	line_existence : ∀ A B, A ≠ B → ∃ l, Incid A l ∧ Incid B l; line_uniqueness : ∀ A B l m, A ≠ B → Incid A l → Incid B l → Incid A m → Incid B m → EqL l m;
cyc	???
vrm	???
cl	???

Alex

пт, 1 мая 2026 г. в 21:08, 'Jans Aasman' via ontolog-forum <ontolo...@googlegroups.com>:

To view this discussion visit https://groups.google.com/d/msgid/ontolog-forum/CABd59doT2RQQ%2BBLN01imy6eUK9v__X-Lke57pB%2BcvqJNszyDpw%40mail.gmail.com.

[Jans Aasman]

Thanks Alex. I'm amazed by what deepseek found. My beloveth Perplexity.ai found *none* of that . I'm going to play with some of those test sets. Cheers, Jans

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

[alex.shkotin]

Welcome, Jans. It would be great to get some CL-formulas to my collection. Cheers, Alex

воскресенье, 3 мая 2026 г. в 05:26:22 UTC+3, Jans Aasman: