# 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:

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.