Introduction

FO[·] (aka FO-dot) is First Order logic with various extensions to allow complex knowledge to be expressed in a rigorous and elaboration-tolerant way. FO[·] facilitates the development of knowledge-intensive applications capable of intelligent behavior [CVVD22]. It uses conventional logic notations as much as possible.

An FO[·] knowledge base (KB) is a set of statements in an application domain. These statements allow distinguishing the satisfying states of affairs (in which the statements are true), from those in which at least one of them is false.

If the statements in the KB are laws of the physical world, then they are true in any physical situations we could possibly be in. If they are a transcription of a statutory law, they are true in any legally-acceptable state of affairs. If they are rules of thumbs about what a good product configuration should be, they are true in states of affairs where the product has all the desired properties. Hence, the statements in a KB describes what is possible, acceptable or desirable, depending on the purpose of the KB.

An FO-dot knowledge base is not a program. It cannot be run or executed. It is not even the description of a computational problem. It is just a “bag of information”, describing certain properties of the application domain.

The information provided in the knowledge base can be used as input to various generic reasoning algorithms: e.g., algorithms to determine relevant questions, to compute consequences of new facts, or to explain them. These algorithms are implemented in reasoning engines, such as IDP-Z3.

These are the current extensions of FO[·]:

Core

Multi-sorted logic with finite data structures and equality

Sugar

Binary quantification, type inference and other convenient notations

PF

Partial functions

ID

(Inductive) definitions

Int

Integer arithmetic, ranges and dates

Real

Real arithmetic

Agg

Aggregates: cardinality, sum, min, max

Infinite

Quantification over infinite domains (including recursive types)

Concept

Quantification over intensional objects

A reasoning engine may support all the extensions, or only a subset. The extensions are loosely coupled, so that each possible combination defines a different language. The dependencies are shown in the following diagram:

flowchart BT subgraph Dependencies direction BT Core --> Sugar --> PF; Core --> ID; PF --> Int --> Agg; Int --> Real --> Infinite; Int --> Infinite; Real --> Agg; Core --> Concept; end;

The grammar of all the extensions combined is described in the FO[.] page.

Other extensions are under consideration for inclusion in FO[·]:

Open

Quantification over open (aka uninterpreted) types

Causal

Causal processes

Cos

Transcendental functions

Unit

Physical quantities with Unit of Measurements

Note

We use the following nomenclature:

  • FO is First Order logic;

  • FO[x,y] (with square brackets) is the concrete language with extensions x,y; it is used to write knowledge bases;

  • FO(x,y) (with parenthesis) is the theoretical language with extensions x,y; it is used to rigorously specify the essential semantics of the extension;

  • FO[·] (resp. FO(·)) is the concrete (resp. theoretical) language with all the extensions described in this document.