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[·]:


Multi-sorted logic with finite data structures and equality


Binary quantification, type inference and other convenient notations


Partial functions


(Inductive) definitions


Integer arithmetic, ranges and dates


Real arithmetic


Aggregates: cardinality, sum, min, max


Quantification over infinite domains (including recursive types)


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[·]:


Quantification over open (aka uninterpreted) types


Causal processes


Transcendental functions


Physical quantities with Unit of Measurements


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.