FO[Core]¶
This chapter describes the syntax and semantics of the minimal language constructs supported by every member of the FO[·] language family. Some of the constraints introduced by this minimal language are removed by extensions such as FO[Infinite].
Goal¶
FO[Core] is a typed (aka multi-sorted) first order logic with equality, if-then-else, and special constructs to facilitate the creation of identifiers and to specify the interpretation of predicates and functions. All types have a finite interpretation, allowing grounding [WMarienD14]. (This constraint is removed in FO[Int] and FO[Real])
Knowledge Base¶
This section describes the high-level structure of a knowledge base.
Lexicon
A Knowledge Base is a text file encoded in UTF-8.
The following character(s) are “white spaces”: they separate tokens, but have no meaning by themselves.
0x09
(tab)0x10
(new line)0x13
(line feed)0x32
(space)comments: string starting from
//
till the end of the line (0x10
or0x13
).
Token |
Pattern |
Example |
---|---|---|
ID |
|
|
NAME_V |
ID |
|
NAME_TH |
ID |
|
Syntax
KnowledgeBase ← VocabularyBlock { (VocabularyBlock | TheoryBlock | StructureBlock) };
VocabularyBlock ← 'vocabulary' [NAME_V] '{' { Declaration } '}';
TheoryBlock ← 'theory' [ NAME_TH [: NAME_V] ] '{' { Assertion } '}';
StructureBlock ← 'structure' [ NAME_TH [: NAME_V] ] '{' { Interpretation } '}';
Well-formedness
The Knowledge Base must have at least one vocabulary and one theory block.
The Knowledge Base may contain other types of block, e.g., procedural blocks to perform reasoning tasks. These blocks are not part of this standard.
If omitted,
NAME_V
(resp.NAME_TH
) is assumed to be the stringV
(resp.T
).The
NAME_V
in a theory (or structure) block must be the same as theNAME_V
of a previous vocabulary block.When the Knowledge Base has several vocabulary (resp. theory or structure) blocks, two vocabulary (resp. theory or structure) blocks cannot have the same
NAME_V
(resp.NAME_TH
).
Semantics
A state of affairs is a static “mental world” that can be communicated by a set of descriptive sentences in natural language (e.g., in English). (A state of affairs is similar to a mental model in cognitive science [JL08])
A knowledge base is a formal description of all the possible (or desirable, or acceptable) states of affairs in a problem domain.
A vocabulary declares the symbols denoting important concepts in a problem domain. Each symbol has an informal meaning in natural language in the problem domain. There are 3 types of symbols: type, function and predicate symbols.
A particular state of affairs is described by giving a total interpretation to every symbol. The set of these interpretations is a total structure. A structure is an abstraction of a state of affairs.
A theory (over a vocabulary) is a set of assertions that are true in every model, i.e., in every structure that are possible (or desirable, or acceptable). A structure in which all assertions are true is a model of the theory.
Many reasoning tasks involve only one vocabulary and theory, but some reasoning tasks, such as “determine if 2 theories are equivalent” require more.
A structure block is a special kind of theory blocks that only contains interpretations of types and symbols. They typically contain observations about a state of affairs.
Example
vocabulary {
// here comes the declaration of types and symbols
}
theory {
// here comes the definitions and axioms
}
structure {
// here comes the interpretation of some symbols
}
Type declaration¶
This section describes how a type is declared in the vocabulary.
Lexicon
Token |
Pattern |
Example |
---|---|---|
ACCESSOR |
ID |
|
BOOL |
either |
|
CONSTRUCTOR |
ID |
|
NAME_T |
ID |
|
NAME_I |
ID or |
‘John Doe’ |
Syntax
Declaration ← 'type' NAME_T [':=' TypeInterpretation] ;
TypeInterpretation ← '{' NAME_I { ',' NAME_I } '}';
TypeInterpretation ← 'constructed' 'from'
'{' ConstructorDeclaration { ',' ConstructorDeclaration } '}';
ConstructorDeclaration ← NAME_I;
ConstructorDeclaration ← CONSTRUCTOR '(' [ACCESSOR ':' ] Type
{',' [ACCESSOR ':' ] Type} ')';
Type ← NAME_T | BOOL;
Well-formedness
A
NAME_T
(resp.NAME_I
,CONSTRUCTOR
,ACCESSOR
) can be declared only once. ANAME_T
cannot conflict with another Type (e.g.,Bool
). ANAME_I
cannot conflict with another Identifier.The 4 sets of
Type
,Identifier
,CONSTRUCTOR
andACCESSOR
strings must be disjoint.Constructors are not recursive:
NAME_T
occurring as argument of aCONSTRUCTOR
must have been previously declared (relaxed in FO[Infinite]).
Semantics
The domain of discourse is a set of objects (aka individuals) in the state of affairs.
Types are disjoint subsets of the domain of discourse. The domain of discourse is the union of the types. All types are finite sets in FO[Core].
A type interpretation gives a unique name to each element of the subset (UNA: Unique Name Axiom). Every element in the subset has a name (DCA: Domain Closure Axiom).
A name can be an identifier or a compound identifier.
A “direct” type declaration consists of a set of identifiers.
A “constructed type” declaration consists of a set of constructor declarations. All the compound identifiers of the constructed type are obtained by applying each constructor in the declaration to each possible tuple of elements of their
Type
arguments (if any).
Examples
type Color := {red, blue, green}
type RGB := constructed from {RGB(Bool, Bool, Bool)}
red
, blue
and green
are the 3 different Color
s. There are only 3 Color
s.
RGB(true, false, false)
is an element of type RGB
. This type has \(2⨯2⨯2=8\) elements.
Function and Predicate declaration¶
This section describes how functions and predicates are declared in the vocabulary.
Lexicon
Token |
Pattern |
Example |
---|---|---|
ANNOT |
|
|
NAME_S |
ID |
|
TIMES |
|
|
TO |
|
Syntax
Declaration ← { ANNOT } NAME_S { ',' NAME_S } ':' Signature;
Signature ← '(' [ Type { TIMES Type } ] ')' TO Type;
Signature ← Type { TIMES Type } TO Type;
Well-formedness
A
NAME_S
can be declared only once. It cannot conflict with another (built-in) symbol (such asabs
in FO[Int]).A
NAME_T
cannot occur in aSignature
before it has been declared.The 5 sets of
Type
,Symbol
,Identifier
,CONSTRUCTOR
andACCESSOR
strings must be disjoint.
Semantics
This Declaration declares one (or more) function symbol and its type signature. The
Type
s beforeTO
specify the domain of the function; theType
afterTO
specify its range.A function whose range is
BOOL
is also called a predicate.Annotations do not have logic meaning, but can be parsed by a reasoning engine. They may be used to, e.g., specify the informal semantics of a symbol, for display to a user. Their use is not specified in this standard.
Examples
convex, equilateral : () → 𝔹
colorOf: Country → Color
[edge of a graph]
edge : Node ⨯ Node → Bool
Import¶
This section declares how declarations can be imported from a vocabulary in another.
Syntax
Declaration ← 'import' NAME_V;
Well-formedness
vocabulary
NAME_V
must have been declared previously in the knowledge base.
Semantics
the declarations in the vocabulary named
NAME_V
are added to the vocabulary that contains theimport
declaration.
Axiom¶
This section describes how logic statements are added to a theory.
Lexicon
Token |
Pattern |
Example |
---|---|---|
AND |
|
|
EQUIVALENCE |
|
|
IMPLICATION |
|
|
IN |
|
|
OR |
|
|
QUANTOR |
|
|
R_IMPLICATION |
|
|
UNARY |
|
|
VARIABLE |
ID |
Syntax
Assertion ← Axiom;
Axiom ← Expression '.';
Expression ← [ { ANNOT } QUANTOR Quantee {',' Quantee} ':' ] RImplication;
Quantee ← VARIABLE {',' VARIABLE} IN Type;
RImplication ← Equivalence [R_IMPLICATION Equivalence];
Equivalence ← Implication [EQUIVALENCE Implication];
Implication ← Disjunction [IMPLICATION Disjunction];
Disjunction ← Conjunction {OR Conjunction};
Conjunction ← Unary {AND Unary};
Unary ← { UNARY } Base;
Base ← 'if' Expression 'then' Expression 'else' Expression;
Base ← { ANNOT } QUANTOR Quantee {',' Quantee} ':' RImplication;
Base ← Symbol '(' [Expression {',' Expression}] ')';
Base ← Identifier | VARIABLE;
Base ← { ANNOT } '(' Expression ')';
Identifier ← 'true' | 'false' | NAME_I;
Symbol ← NAME_S;
Symbol ← CONSTRUCTOR | ACCESSOR | 'is_{CONSTRUCTOR}';
Here, 'is_{CONSTRUCTOR}'
represents any string constructed from 'is_'
and a CONSTRUCTOR
,
e.g., is_RGB
.
Well-formedness
Each
NAME_T
,NAME_S
strings must have been declared in the vocabulary. EachNAME_I
,CONSTRUCTOR
andACCESSOR
must have been declared before occurring in aBase
.Each expression has a type based on the declarations in the vocabulary. An axiom must be a boolean expression. The elements of an expression must have the appropriate types, as specified in the symbol declarations or as required by the built-in connectives.
Each variable must occur in the scope of a quantifier that declares it.
Semantics
The expressions above have their usual mathematical / logic meaning. (See also the semantics of FO(Core) below)
The production rules above define the precedence of the operators.
An
is_{CONSTRUCTOR}
string denotes a unary predicate that says whether the argument was constructed withCONSTRUCTOR
.When
ACCESSOR
is the name of the n-th argument ofCONSTRUCTOR
according to its declaration, it denotes a function that takes an objectO
created byCONSTRUCTOR
, and returns the n-th argument that has been applied to the constructor to constructO
. The occurrences ofACCESSOR
in an expression must be properly guarded to ensure it is applied to appropriate arguments.
Examples
In ∀x,y ∈ T: p(x,y) ∨ f(f(x))=y.
, x
and y
are variables of type T
.
Assuming type Color := {RGB{red: Bool, green: Bool, blue: Bool}}
,
is_RGB(RGB(true, false, false))
is true
and
red(RGB(true, false, false))
is true
.
Symbol Interpretation¶
This section describes how the interpretation of a function or predicate
is added to a theory
or structure
.
Syntax
Assertion ← Interpretation;
Interpretation ← NAME_T ':=' TypeInterpretation '.';
Interpretation ← NAME_S ':=' Value '.';
Interpretation ← NAME_S ':=' SymbolInterpretation '.';
Value ← Identifier;
Value ← CONSTRUCTOR [ '(' Value {',' Value } ')';
SymbolInterpretation ← '{' TupleValue { ',' TupleValue } '}';
SymbolInterpretation ← '{' TupleValue TO Value { ',' TupleValue TO Value} '}' [else];
TupleValue ← Value;
TupleValue ← '(' Value { ',' Value } ')';
else ← 'else' Value;
Well-formedness
A
NAME_T
orNAME_S
can be interpreted only once.All types must be interpreted, in the vocabulary or in a theory/structure.
Each
NAME_I
,CONSTRUCTOR
andACCESSOR
must have been declared before occurring in aValue
.The interpretation can be a single value only for nullary predicates or functions (i.e., with an arity of 0).
The number and type of values in an interpretation must match the type signature of the
NAME_S
being interpreted.The number and types of values in a compound identifier must match the type signature of the
CONSTRUCTOR
.The
TO
element is mandatory in function interpretations, and prohibited in predicate interpretations (relaxed in FO[Sugar]).
Semantics
These assertions define the interpretation of types, predicates and functions.
For a type, the assertion has the same semantics as in a type declaration
For a predicate, the set of
TupleValue
is the set of values for which the predicate istrue
; the predicate is false for any otherTupleValue
; for nullary predicate, the unique Value can betrue
orfalse
.For a function, the assertion maps tuple of arguments to their value. The value after
else
is the value given to the function for tuples of arguments that are not in the enumeration. For nullary symbols, the interpretation can be a unique value.
Examples
Color := {red, blue, green}.
node := {A, B, C}.
colorOf := {A -> red, B -> blue} else green.
edge := {(A,B), (B,B)}.
convex := true.
FO(Core) abstract language¶
This section contains the formal theory of the FO(Core) abstract language.
The translation between the abstract language and the concrete language is not provided. However, corresponding concepts in the abstract and the concrete language are denoted by the same words: this should allow the reader to establish the correspondence by himself.
\(T\) is a set of type-symbols. It contains type-symbol \(𝔹\).
A n-signature is a (n+1)-tuple of type-symbols, noted \(T_1 ⨯ \dots ⨯ T_n → T\), where \(0 \leq n\). (A 0-signature is noted \(() → T\))
A vocabulary \(Σ\) is a set of (symbol \(σ\), n-signature) pairs.
A typing function \(γ\) is a function that maps variables to type-symbols. For a given \(γ\), we define \(γ[x : T]\) to be the function \(γ′\) identical to \(γ\) except that \(γ′(x) = T\).
The type of string \(φ\) (over \(Σ\)) given a typing function \(γ\), noted \(τ(φ, γ)\), is a type-symbol partially defined by induction as follows (terminal symbols are underlined for clarity):
\(φ\) |
\(τ(φ, γ)\) |
if |
---|---|---|
\(\underline{true}\) |
\(𝔹\) |
|
\(\underline{false}\) |
\(𝔹\) |
|
\(x\) |
\(γ(x)\) |
x is a variable |
\(σ\underline{(}t_1\underline{,} .. \underline{,}t_n\underline{)}\) |
\(T\) |
\((σ,T_1 ⨯ \dots ⨯ T_n → T) \in Σ\) |
\(φ\underline{∨}ψ\) |
\(𝔹\) |
\(τ(φ,γ)=𝔹\) and \(τ(ψ,γ)=𝔹\) |
\(\underline{¬}φ\) |
\(𝔹\) |
\(τ(φ,γ)=𝔹\) |
\(\underline{∃} x \underline{∈} T\underline{:} φ\) |
\(𝔹\) |
\(x\) is a variable and \(τ(φ,γ[x:T])=𝔹\) |
\(t_1\underline{=}t_2\) |
\(𝔹\) |
\(τ(t_1,γ)=τ(t_2,γ)\) |
\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\) |
\(T\) |
\(τ(φ,γ)=𝔹\) and \(τ(t_1,γ)=T=τ(t_2,γ)\) |
otherwise |
undefined |
Let \(∅\) be the typing function with empty domain. We say that \(φ\) is a well-formed formula of type \(T\) over \(Σ\) if \(τ(φ,∅)=T\). A sentence is a well-formed formula of type \(𝔹\).
This table shows how to extend the syntax with convenient notations:
Convenient notation |
Equivalent formula |
---|---|
\(φ\underline{∧}ψ\) |
\(¬(¬φ∨¬ψ)\) |
\(φ\underline{⇒}ψ\) |
\(¬φ∨ψ\) |
\(φ\underline{⇐}ψ\) |
\(φ∨¬ψ\) |
\(φ\underline{⇔}ψ\) |
\((φ∧ψ)∨(¬φ∧¬ψ)\) |
\(\underline{∀}x \underline{∈} T\underline{:}φ\) |
\(¬∃x∈T:¬φ\) |
A (total) structure \(𝓘\) over \(Σ\) consists of :
an object domain \(D\) containing \(𝔹^𝓘\), the set of booleans;
a mapping of type-symbols \(T\) to disjoint subsets \(T^𝓘\) of \(D\); \(D\) is the union of all \(T^𝓘\);
a (total) mapping from symbols \(σ\) with n-signature \(T_1 ⨯ \dots ⨯ T_n → T\) to (total) functions from \(T_1^𝓘 ⨯ \dots ⨯ T_n^𝓘\) to \(T^𝓘\).
Note: Identifier
and CONSTRUCTOR
strings are function symbols whose interpretation have the following properties:
All well-formed ground terms of type \(T\) built exclusively with them uniquely identify an element of \(T^𝓘\).
Every element of \(T^𝓘\) is uniquely identified by a well-formed ground term of type \(T\) built exclusively with them.
We define a variable assignment \(ν\) as a mapping of variables to elements in \(D\). A variable assignment extended so that the mapping of \(x\) is \(d\) is denoted \(ν[x : d]\).
The value of formula \(φ\) in \((𝓘,ν)\), denoted \(⟦t⟧^I_ν = v\), is an element of \(D\) partially defined by induction as follows:
\(φ\) |
\(⟦φ⟧^I_ν\) |
if |
---|---|---|
\(\underline{true}\) |
\(true\) |
|
\(\underline{false}\) |
\(false\) |
|
\(x\) |
\(ν(x)\) |
x is a variable in the domain of \(ν\) |
\(σ\underline{(}t_1\underline{,} .. \underline{,}t_n\underline{)}\) |
\(σ^𝓘(⟦t_1⟧^I_ν, .. ,⟦t_n⟧^I_ν)\) |
\((σ,T_1 ⨯ \dots ⨯ T_n → T) \in Σ\) |
\(φ\underline{∨}ψ\) |
\(false\) |
\(⟦φ⟧^I_ν\) is defined and false |
\(φ\underline{∨}ψ\) |
\(⟦φ⟧^I_ν ∨ ⟦ψ⟧^I_ν\) |
\(⟦φ⟧^I_ν\) and \(⟦ψ⟧^I_ν\) are defined |
\(\underline{¬}φ\) |
\(¬⟦φ⟧^I_ν\) |
\(⟦φ⟧^I_ν\) is defined |
\(\underline{∃} x \underline{∈} T\underline{:} φ\) |
\(∃d ∈ T^I : ⟦φ⟧^I_ν[x:d]\) |
\(⟦φ⟧^I_ν[x:d]\) is defined for every d in \(T^I\) |
\(t_1\underline{=}t_2\) |
\(⟦t_1⟧^I_ν = ⟦t_2⟧^I_ν\) |
\(⟦t_1⟧^I_ν\) and \(⟦t_2⟧^I_ν\) are defined |
\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\) |
\(⟦t_1⟧^I_ν\) |
\(⟦φ⟧^I_ν=true\) and \(⟦t_1⟧^I_ν\) is defined |
\(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\) |
\(⟦t_2⟧^I_ν\) |
\(⟦φ⟧^I_ν=false\) and \(⟦t_2⟧^I_ν\) is defined |
otherwise |
undefined |
Notice that \(φ\underline{∨}ψ\) and \(\mathbf{\underline{if}~} φ \mathbf{~\underline{then}~} t_1 \mathbf{~\underline{else}~} t_2\) have non-strict semantics.
We say a total structure \(𝓘\) satisfies sentence \(φ\) iff \(⟦φ⟧^I_ν=\mathit{true}\) for any \(ν\). This is denoted \(𝓘 ⊧ φ\). Structures \(𝓘\) that satisfy \(φ\) are called models of \(φ\).