Definitions About KRLs in General, And FL in particular _________________________________________________________________________________________

Dr Philippe A. MARTIN

Table of Contents

1. Informal Definitions 2. Conventions, Notation And Abbreviations

1. Informal Definitions

Name / identifier. A name can have many senses (hence can refer to many things) while an identifier has only one meaning. Anything can have many names and many identifiers, even for a same person.

Information object: interpretable/un-interpretable representation of something.
Un-interpretable information object: one that does not follow enough syntactic and/or lexical rules to be interpreted (for formal expressions the grammar of the used language can be used to determine this).
Interpretable information object: expression or command. In a KR, this is either a type or an individual. Indeed, in a KR, an expression is either a term or a sentence, and a command is a statement (asserted sentence).
Fully declarative expression: information object that is not a command and that does not include a command. In a KR, this is either a term or a sentence, or in other words, either a phrase (sentence or expression referring to a sentence) or a term that does not refer to a phrase.
Not fully declarative expression: something that is not a command but still includes a command. Various ways to define "declarative" could also be used based on various behavioral properties but this will not be done in this document.
Sentence: information object that is assertable, i.e. that can be assigned a truth value. A sentence may be asserted or not, and may be refered to by an identifier. A sentence may contain 0, 1 or several relations.
Term: either a value or a reference.
Atomic expression (and "atomic term"): atomic reference (name or identifier for something, e.g. for a sentence) or atomic value (e.g. 3.14).
Non-atomic expression: expression (e.g. the destination of a relation, a function/procedure call, a query) that permits to compute/retrieve or specify a term. In a KR, it is declarative, hence a non-atomic term.
Phrase: sentence or expression referring to a sentence.
Command: asserted phrase or assertion (i.e. addition), modification or removal of a phrase.
Statement: asserted phrase or assertion of a phrase. In a KR (i.e. with logic-based approaches) a statement is a asserted phrase.
Relation: sentence that relates information objects.
Type (term): term that can have an instance, i.e. that can be destination of a `type' relation. Examples: the 1st-order type `Person' and the second-order type `Type'.  A type is either a concept type (e.g. Type) or a relation type (e.g. type).
Instance (term): term that has (i.e. that is source of) a `type' relation, i.e. a relation of type `type' (alias `instance_of'), e.g. `Tom' (instance of `Person') and `Person' (instance of `Type'); `instance' is the inverse relation type of `type'.
Subtype (term): source of a manually set or automatically deduced `subtype' relation; informally, a term ?st is subtype of a type ?t iff every instance of ?st is instance of ?t.
Individual (term): term that cannot have an instance, nor then a subtype, e.g. `Tom'. However, an individual may have a sub-term, or more precisely a sub-individual, e.g. `Tom_in_2010'.

Meta-statement: statement about a statement, i.e. statement including another one.
Meta-sentence: sentence about a sentence.
Embedding part of a meta-sentence: part of the meta-sentence without the embedded sentence.
Contextualized sentence: embedded sentence which would be false (according to the creator of the sentence if it is a belief) without at least one of its embedding sentences.
Context of a sentence: the embedding sentences that cannot be removed without the result becoming false (according to the creator of the sentence if it is a belief).
Sentence with its context: sentence plus its context if it has one.
Minimally-complete sentence: "sentence with its context" which would be false (according to the creator of the sentence if it is a belief) without any of its parts: term(s) or embedded sentence(s).

Formal information object: information object which, given its syntax or embedding module (e.g., document or sentence), can automatically be recognised as refering to only one meaning. This meaning may or may not be explicitly defined, hence it might be known only by the author of the information object. Identifiers are formal terms.
Informal term: term which is not formal.
Formal, semi-formal or informal sentence: a sentence which is a well-formed knowledge representation (KR; cf. next paragraph) is formal if it only contains formal terms, and semi-formal otherwise. A sentence which is not formal nor semi-formal is informal.
In this document:

• Every formal and semi-formal object i) is a formal term or a well-formed KR, ii) is by default in the FL notation (i.e., if another notation is used, it must be specified in FL at the beginning of each KR or it must be specified via a KR parsing command before the KRs that are not in FL), and iii) is displayed in the courrier font.
  If a (semi-)formal object is directly within an informal paragraph, i.e. if it is not meant to be parsed but is meant as an example or a reference, i) it may be hyperlinked to what it refers, and ii) the FL delimiters needs not be used around it (since the hyperlink and/or the courrier font visually delimit it).
  Here is a list of delimiters usable in FL (a summary/synthesis is given below; these deimiters are mandatory when an object needs to be delimited to be distinguished from other objects or if the kind of the object is not explicit). Remembering (or understanding) this list is a priori not required for understanding the KRs in this document since the used kinds of the objects will be obvious given its embedding objects and, if needed, the comments.
  1. For any (semi-)formal object (although if it is one of the objects below, this is a useless addition):
     - '(' on the left and ')' on the right, or
     - '`' (left single quote) on the left and
       either '\'' (straight single quote) or '´' (right single quote) on the right.
     E.g., (a car color: a white) or `a car color: a white' for referring to "a white car".
  2. For a (semi-)formal sentence:
     • '[' on the left and ']' on the right, as in [a Cat] and [a Thing, type: Cat] which both mean "there exists a cat", or
     • ".`" on the left and '\'' or '´' on the right, as in .`there is a Cat' or .`there is a Thing with type Cat' which are both equivalent to [a Cat]. When this second case is used, the sub-KRL of FL named Formalized-English (FE) should rather be used. FE is just FL with, when possible, some syntactic sugar that makes it look more like English.
  3. For an informal sentence: '"' or '\'' (straight double/single quote) on the left and the same delimiter on the right, as with "this sentence is informal".
  4. For an informal term: i) on the left, '^"' for a type and '.^"' for an individual, and ii) '"' on the right; as with ^"Cat", ^"Cat that is white" and ."Tom the cat".
  5. For a (semi-)formal term that is an anonymous type full-definition (via a relation path expression or not) (if the type is a function type, this is a lambda-abstraction; if the type is a relation type, this is a kappa-abstraction):
     • '^(' and ')' for an anonymous full-definition that is not in FE:
       • the source may be explicit, as with ^(Cat color: a white) which could be used as a definition for a "white_cat";
       • the source may also not be made explicit (as for object/frame definitions in almost all object/frame notations) if '^(.' is used, e.g. ^(. color: a white) is equivalent to ^(Thing color: a white).
     • '^`' on the left and '´' or '\'' on the right for an anonymous concept type full-definition in FE, as with ^`Cat with color a white'. Note: the anonymous definition must have at least one space within it for the parser to distinguish it from a type with optional delimiters (cf. 2nd case in the last point).
  6. For a formal term identifier, the left outer identifier is "^'" for a type and ".^'" for an individual. The right one is ''' or '´'.
     • If the identifier is written in FE-for-identifiers (a sub-KRL of FE and thus of FL) – and hence encodes an anonymous definition for it – '^^' is used instead of '^' Examples (with all the delimiters): ^^`Process_with_fairness', ^^`Man_with_part_2_eye-with-color-a-blue_and_agent_of_a-singing' and ^^`Man with part 2 eye-with-color-a-blue and agent of a-singing'.
     • Otherwise, if the identifier has no non-alphanumeric character (e.g. a space) within it, the delimiters are optional. E.g.: .^`Tom_the_cat´ and, to name a statement, .^`There_is_a_cat´ (There_is_a_cat can be used without delimiters if it has already been defined as referring to a sentence such as "There is a cat").
  Note: as in other KRLs, a phrase that is source/destination of a relation, function or operator (except for "and") is not asserted. Conversely, a phrase is asserted if the sentence is an un-embedded sentence (an embedding via an "and" operator does not count). However, FL provides an exception: by prefixing a phrase (or a relation the phrase is source of) by ". " (or ".") the phrase is asserted regardless of its embedding level. This for example permits [.?p => ?p2] and [?p .=> ?p2] to be equivalent (and shortcuts for) [?p [?p => ?p2]].
• By default, the creator of every object in this document is "Philippe Martin", the author of this document. `pm' is one formal term defined to refer to this author. FL offers various ways to specify the creator of objects. One way to specify the creator of an identifier is to prefix this identifier by an identifier of the creator, as in the following example: pm#formal_term.

Sentence  //'&'(inv:*):Sit->SemDescr(e.g. Prop, Name);  "&.&"(inv:*.*):SemDescr->LexicalDescr.
  Informal_or_mostly-informal_sentence  //value variables (vv) may be prefixed by $ (-> ~ sh, not KIF)
  //Warning: informally I also used these to delimit non-token expressions, not just sentences
    .._unreified_wo_vv_subst         '.. .#.. ..'       e.g. 'there exists a pm#cat'
    .._unreified_with_vv_subst       "...${..}.."       e.g. "   ${exists_a} pm#cat"
    .._reified_wo_vv_subst          &'.. .#.. ..'       e.g. `&.&"a cat" part: 5 char'
    .._reified_with_vv_subst        &"...${..}.."       e.g. `the State &"${exists_a} cat"' 
  Formal_or_semi-formal_sentence //for full quoting (no vv subst nor fct calls), use \ before ` and [
            //for semi-quoting (LISP backquoting and then ','), use "\$" and then "\\" instead of ',' 
       //in a file, if `...' is alone (no relation): this is an assertion
       //           otherwise this is not an assertion unless prefixed by '.'
    .._unreified_in-FE               `...'              e.g. `a Cat'   //not .`a Cat' nor (a Cat)
    .._reified_in-FE                &`...'              e.g. &`a Cat' believer_[*.->.]: pm
    .._unreified_not-in-FE           [..]               e.g. [ [a pm#Cat] [a Dog] ]
    .._reified_not-in-FE            &[..]               e.g. `&[a Cat] *_[believer:pm]', `*(&[a Cat])'
  //??? Sentence evaluation ???     ^[...]              //what is that? not a command/fctCall!
  //  see webk.org/kb/it/p_securing/d_securing_CERT.html
  Embedded-sentence_assertion       . ...               e.g. [.?p =>?p2]<=>[?p . =>?p2]<=>[?p :=>?p2]
    //warning: != indivs(.^'Tom the cat' .^'a Cat is on a Mat')  != descriptive_implication(".=>/.~>")
  Constraint/directive              !_! ...               e.g. !_! no Forward_declaration;
    Descriptive_constraint          !_!dc ...             e.g. !_!dc [Mother range: a Female_animal]
    Prescriptive_constraint         !_!pc ...             e.g. !_!pc [each Human  part: an ID]

Term  //'&'(inv:*|$): Var/fct->Value + Sit->SemDescr;  "&.&": SemDescr->LexicalDescr.
  Token                    //so parenthesis are necessary for composing reifications
    Variable                                            e.
      Value_variable                 (*pFct_(..)):= ..  //no prefix for vars local to a JS like fct
        Macro/shell-like_variable    $..                e.g. $var  //to initialize: \$var or &$var
      Declarative_var
        Free_variable                ^..                e.g. ^var
        Non-free_variable
          .._distributive            ?..                e.g. .{1..* Thing ?a} ?as @.?as
          .._collective              @_?..              e.g. .{?x,?y} ?member @_?collMembers @.?set
          .._cumulative              @.?..                   (see below for details)
          .._sequence                @*?..              e.g. .{Joe,Tom} @*?seqMember 
    Constant
      Identifier
        Informal_identifier (i.e. declared-or-not name for a type/indiv)
          .._for_a_type             ^".."  ^'..'        e.g. ^"Cat that is white"
          .._for_an_individual     .^".." .^'..'        e.g. .^"Tom the cat" .^"a Cat that is on a Mat"
                                                             Proposition .^"a Cat is on a Mat"
        Formal-or-semi-formal_identifier //!=  ^Univ_var  ^`...'/*Anonymous-type_definition*/
          .._in_FE-for-identifiers ^^NameThatIsAlsoAnFEexpr or ^^`FE expr that is also a name'            
            .._for_a_type(asLambda) ^^`..'  ^^`..´      e.g. ^^`Cat_with_color_a_white'
            .._for_an_individual   .^^`..' .^^`..´          .^^`Tom the cat' .^^`a Cat with place a Mat'
                                                            Proposition .^^`a Cat has for place a Mat'
          .._not_in_FE-for-identifiers
            .._with_non-alphanum    ^`..' .^`..´        e.g. ^'White Cat'   .^'a Cat that is on a Mat'
                                                             ^'pm#>=' ^'>=' .^'a Cat is on a Mat'
            .._without_non-alphanum (idem but optional) e.g. Cat, pm#Tom, Tom, A_Cat_that_is_on_a_Mat
                                                             ^`Cat', .^`Tom',  There_is_a_cat_on_a_mat 
      Value_token //Literal
        String                                          //reminder: *(inv: &)
        .._woSubst(^..'..',$(..)$)  &.&'..'  &^`..'     //String for Sentence / type informal name
        .._wSubst (^.."..",$(..)$)  &.&"..${..}..?(..)" e.g. *"a ${c} de ?(g) hi"
        Number
  Term_that_is_not_a_token 
    ..._context_related
      context  // [..]:semantic,  &[..]/&->:lexical(display rel),  *[..]/*->:index/expl. rel 
               //              or: [.. &-> ..], e.g. `a Cat (length _[length &.&:6]) _[.&.&->.]: 3'
               //                                    `a Cat _[ _[relOnThisCtxt:...] believer: ..]' 
               //use "[] descr_instr: .._[..]" if referred statement not-automatically found
               //  [pm#English#not] <=> [user: pm;  English#not] <=> [[__ KRL: FL] &.&(pm#English#not)]
               //  <=> [ &.&[__ notation: FL  Notation_in_which_a_colon_plays_the_role_of_diese_in_FL
               //      ] pm:English:not ]     //in FL, the role of '#" is only by default
        .._postfixed_1out           _[..]               e.g. [a Cat] _[time: 2018, place: USA]
        .._postfixed_2out          __[..]               e.g. ?x ?r: ?y __[time: 2018, place: USA]
        .._prefixed_1out             [_..]              e.g. [_ time: 2018, place: USA] [a Cat]
        .._prefixed_2out             [__..]             e.g. [__ time: 2018, place: USA] ?x ?r: ?y
    ..._definition-related
      Type_signature                 
        // - no * in sign. since specialization may add param; all ? (unary) by default
        // - r .(1stOrderType1,a 2ndOrderType2), e.g.:  transitiveRel.(a ?t, a ?t)
        // - functional[applic.] (any->1):  r (t1, 1 t2)  or  r (t1 -% t2) 
        //    surjection (any->1, 1..*<-any): r (t1  1..* ->  t2) 
        //    injection (any->1, 0..1<-any) //so diff->diff (so =<-=), 1-to-1 fct, !bij:1-to-1 assoc
        //    bijection (any->1, 1<-any): r (t1 <-> t2)
        // - inverse functional: r (t1 <- t2) 
        // - conditional: [rX ^rx   rR: rY ^ry] => [ rR .(rX, rY) ] iff the premise is 
        //      implicitly/explicitly confirmed so a way to represent the corresponding compiling
        //      option is: ... [rX ^rx  rR: rY ^ry] input of: (a compilation time: Now) ...
        Routine-or-RT_signature      .(.., ..)          e.g. fctRel .(Thing ?x, ?y, @*?seq -% ?z)
        CT_signature//w.(o.)rels     .[.., ..]          e.g. Agent .[Process ?p, Object ?o]
        CT_structural_signature      .part[.., ..]      e.g. IF_expr .part[IF_op, %(..), ?res] 
      Anonymous-collection_def.     ^{..}               e.g. ^{Cat color: a white},  ^{[a cat]
      Anonymous-type_definition     ^(.. ..), ^`.. ..'  e.g. ^(Cat color: a white) but not ^Cat
      Rel_definition_via_graph       r .(.. -% ..)         :=|:=> ... //'-%'forArrow/Sig,'-:'forRel/Def
      Fct_definition_via_graph       f .(.., ..) -%|-> ?x  :=|:=> ... ValueGeneratorFct !iterator
        Value(Itero)GeneratorFct_def f*...              e.g. f *.(T1,T2),  T1 f*.(T2)-% T3){...}
      Def_via_rel+inference          .. r :(=|-)(>)(.) ...  //for inferences;  seeAlsoNextTable
        every(:*= :*=>) any(:D=>) each(:=. :.=> :100%=>)  //extensionalSup: _/.
        (":.":onlySup/sub/equivTypes; ":=|:=>":every/any(byDefault)/each for type/implic)
      Def_via_rel+descrCstr          .. r :=~|:=~>  ... //descr cstr: x =~> y //only / signature
      Def_via_rel+prescCstr          .. r :=~.|:.=~>... //presc cstr: x.=~> y //not using inferences
      TypeBranchGenerator @^         .. @^( .. )        e.g. Entity_indiv = ^@(Entity exceptFor: Type)
    ..._other_relation/fct-related    //RelsGenerator = virtual|calculated_rel_assertion
      RelsGenerator(def)prefix @!!   r @!!(..-% ..):= .. e.g. type@!!(T1,T2 ?t2):=[if...then?t2=..]
                        infix  @..   ... r@..(...): ... e.g. T1 type@..(T2 ?t2) :=[if...then?t2=..] 
      ComplexRelNodeBeginDelim       :_ rt1 + rt2 : rd1 rd2   or   :_{rt1,rt2}: rd1 rd2 
                                       (rt1 + rt2): rd1 rd2 
      FctCall_or_relation //prefix by '.' if rel(s), '°' if named args, '^' if descr
                          //CT-def instantiation called as fct (or with '^.' as prefix)
      .._with_prefixed_1out_op       ?r _(.., ..)       e.g. fct_(?x, ?y, @*?seq, ?z) 
                              _descr ?r ^_(.., ..)      //cf. hidden comment here   
      .._with_prefixed_1in_op        (_. ?r .., ..)     e.g. (_. ?r ?x, ?y, @*?seq, ?z)
      .._with_postfixed_1out_op      (_ .., ..) ?r      e.g. (_  ?x, ?y, @*?seq, ?z) ?r
      .._with_postfixed_1in_op       (._ (.., ..) ?r)   e.g. (._ (?x, ?y, @*?seq, ?z) ?r)
      .._with_infixed_op_2args       .. ?r: ..          e.g. ?x ?r: ?y
                                     .., ..: ..         e.g. ?x,_^(..): ?y   
                                     .. :_(..): ..      e.g. ?x :_^(..): ?y //neverMind rels abbrevs 
                                     .. :_{..}: ..      e.g. ?x :_{/^,spec}: ?y //many ttypes/rel
                                     .. :_[..: .., ..   //set of rels, e.g. from a same source
                                          ]_[..]        // or for specializations 
        .._with_infixed_op_Nargs     (: .. :?r ..)      e.g. (: ?x ?y :?r ?z)
      RelType_path_expr              ^-(..)             e.g. [Tom ^-(part+): {a Leg} ?l @.?legs]
                                                              ... ^-(r1+ ^. r2): ... 
      RelTypeAndDest_path_expr       .. ^. ..           e.g.  Tom ^. part+  ?TomPart @.?TomParts 
        FunctionalRel_access/name    .. _._ ..          e.g. &.&`Tom _._ SS_id' _._ length
        //forEach method=1stParamOf  .. _._ ..          e.g. o1_._fct_(o2) <=> fct_(o1,o2) 
    ..._other
      Collection                               //see below: distributive interpretation (no prefix)
        Anonymous-collection_def.   ^{..}               e.g. ^{Cat color: a white},  ^{[a cat]}
        Set (un-ordered; distr.)     {.., ..}           //  collective (prefix: "Coll", "@_", "_"),
          Keyed_set                  {k1:v1, ..}        //  cumulative (prefix: "Cuml", "@.", ".")
                                                        //  e.g.: .AND{each ^(...)}
          Exclusion-character_set    {^ ..}             e.g. {^ a-z}: any character but 'a'..'z'
          .._with_prefixed_1in_op    {_ ...}            ??
        List+Intervals (ordered;default:distr)          //the above prefixes also usable here
          List_with_possible_substs  %[..,..[  %(..,..) e.g. .%]0.1, 1 to 42[, _%[1 ^- 42[, %[1^-42]
          Semi-quoted_list         \$%[..\\$..[         //as in Lisp but "\$"for'`' and "\\$"for','
          Fully_quoted_list         \%[..,..[           //as with Lisp quote

KR. Each KR relates information object by relations in a way that can automatically be translated into a logic formula. Hence, the KR language (KRL) used for writing KRs has a formal syntax (alias, notation or unambiguous concrete grammar) and a formal semantics. In this document, two notations are used for writing KRs: i) FL, and ii) the Peano-Russel notation (PRN) classically used in logics.
Here are simple examples to introduce the way to read FL (later precisions will be given via comments; those are either prefixed by "//" or are within "/*" and "*/", as in C or Java):

• `Tom type: Cat' can be read "Tom has for type Cat", which means that "Tom is a cat". Translation in PRN: `type(Tom,Cat)' or `Cat(Tom)'. From a graph-oriented viewpoint, KRs are set of relations, each one composed of one relation node relating concept nodes. Here, the KR has one relation composed of the relation node "type:" – itself composed of the relation type "type" and an implicit existential quantifier – and two concept nodes, each one composed of only one term (no associated quantifier).
• `Tom type: Cat Male_entity, color: a Grey a Black' can be read
  "Tom has for type Cat and Male_entity, and has for color a Grey and a Black",
  which means that "Tom is male cat whose color is (one shade of) grey and (one shade of) black". Translation in PRN: `∃g Grey(b) ∃g Black(b)  Cat(Tom) ∧ Male_entity(Tom) ∧ color(Tom,b) ∧ color(Tom,g)'. Here, from a graph-oriented viewpoint, the KR has 4 relations (2 of type "type") and 4 concept nodes (one is "a Black", where "a" refers to the existential quantifier; this node thus refers to an anonymous instance of the type Black).
• `Tom part: (a Leg color: a White)' can be read "Tom has for part a Leg which has for color a White", which means "Tom has a leg that is (at least) white".
• More generally, the syntactic form
  "SourceConceptNode relationNode1: DestConceptNode1a DestConceptNode1b, relation2: DestConceptNode2a DestConceptNode2b"
  can be read "SourceConceptNode has for relationNode1 DestConceptNode1a and DestConceptNode1b, and
      has for relationNode2 DestConceptNode2a, and has for relationNode2 DestConceptNode2b"
  while the form "C1 r1: (C2 r2: C3, r3: C4)" can be read
  "C1 has for r1 C2 which has for r2 C3 and for r3 C4".
• Both `any Cat part: a Leg' and `Cat part: a Leg' can be read "any Cat has for part a Leg" because, when the source of a relation is an unquantified type and the signature of the relation type does not include (a variable prefixed by) ".?" in its specification for the source, the default quantifier for the source is `any'. Examples of relation types that have a signature including ".?" are `equal_or_equivalent' and relation_from_an_Information-object (e.g., `definition, `supertype', `=>'). In FL, there are two universal quantifiers – `every' and `any' – because the last one is an abbreviation for "by definition, every". Unlike other sentences, a definition is "true by definition". However, a set of definitions may be inconsistent. Inconsistencies in the KB are signaled to the user when they are detected.

KRs support automatic logical inferencing, and thus automatic KR comparison, search, merge, etc.
Reminders. Every formal information object in a KR is either a `type' (e.g. Cat, part) or an `individual' (e.g. Tom; any relation is also an individual). Every relation is a sentence. Every type is either a concept type (e.g. Cat) or a relation type (e.g. part).
In this document, only `binary relation_s' are used (they are called `binary predicate_s' in 1st-order logic and `triples' or `property instance_s' in RDF).

KR-based command:

• KR assertion: KR explicitly or implicitly prefixed by an assertion operator such as “assert”.
• KR query: KR prefixed by a query operator such as “gSpec” (which looks (in the given/default KB) for the specializations of the parameter KR.
• KRs import command: one specifying that a parameter file/module should be parsed when the import command is encountered.
• KR parsing command: one helping the parsing the KRs that follow the command (until another command gives different specifications), e.g. one specifying that the following KRs have particular implicit (i.e. “by defaut”) parts. The use of these commands eases the writing and reading of KRs by people.
• ...

(Unidirectional) Rule: statement that only supports modus ponens, not modus tollens.
Checking constraint: unidirectional rule only usable for checking purposes, not inferencing.
Descriptive constraint: checking constraint that is not prescriptive.
Prescriptive constraint (alias knowledge entering constraint): checking constraint ensuring that particular statements are not due to inferences, hence checking constraint not exploiting all possible inferences.
Ontology Design Rule (ODR): checking constraint ensuring that a particular "ontology design best practice" is followed.
Ontology Design Best practice: one of the best ODPs to achieve particular good criteria.
Ontology Design Pattern (ODP): how something can be represented to fulfill particular criteria.
All of this is formally categorized in Section 0.3.2.3.

2. Conventions, Notation And Abbreviations

Some conventions:

• Identifiers of relation types begin by a lowercase initial.
• Identifiers of individuals begin by an uppercase (except for abbreviations, e.g. "pm").
• Identifiers of concept types begin by an uppercase but, in informal sentences they may also have initials in lowercase.
• In informal sentences, including outside KRs, "/" means "or" and "|" means "alias".

About the notation (FL). As in some other KR notations:

• A variable identifier is prefixed by the character '?' (as in "?var") when its quantifier is made explicit.
  A variable identifier is prefixed by '^' (as in "^var") when the variable is implicitly universally quantified.
• Unless quoted, identifiers should normally only includes alpha-numeric letters plus '_', '-' and '#'.
• Binary relation nodes (hence, between 2 concept nodes) are usually composed of the relation type identifier followed by ':'. However, FL allow many abbreviations abbreviations (which do not follow the previous rule).
• To associate a signature to a type (of relation, function and, in FL, concept),
  the following form is used: TYPE .(PARAMETER-TYPE1, PARAMETER-TYPE2, ...)
• A function call generally uses the prefixed form TYPE _(PARAMETER-TYPE1, PARAMETER-TYPE2, ...) but there is also a postfix form and an infix form. Furthermore, the characters '+', '-', '*' and '/' can respectively be used for the usual infix abbreviated forms of calls to the functions `add', `minus', `multiply' and `divide', if the parser can distinguish theses abbreviations from characters composing identifiers (one way to make sure of that is to use spaces around these abbreviations).
• Collections (sets, bags, ...) are delimited by '{' and '}' (as in "{Joe,Mary}"). Collections may be prefixed by one type to precise the collection, e.g. "Bag{Joe,John}". By default, collections are interpreted as sets, thus "{Joe,John}" implies that Joe and John are not the same person, while "Bag{Joe,John}" does not. In FL, by default, collections are interpreted distributively, thus "[{Joe,John} type: Person]" is equivalent to "[Person type of: Joe John]". In FL, the interpretation of a collection may be specified explicitly by prefixing it (or its type) with the keyword "Distributive_collection" (or "Distr" as in "Distr{Joe,Mary}") or "Collective_collection" (or "Coll" or "@_" or "_") or "Cumulative_collection" (or "Cuml" or "@." or "."), as in "[.{Joe,Mary} size: 2]"). "Cumulative" means that the relations from/to the collection are about it, not about its members. "Collective" is like "distributive" except that, for each relation from (resp. to) the members, "collective" also indicates that the destination (resp. source) of the relation is unique for all the members, i.e. they "share" it (this may also be viewed as "participating together" to what is expressed by the relation). E.g. "Joe and Mary dance together" may be represented as "[Coll{Joe,Mary} agent of: a dance]" or `there is a dance that has for agent {John, Mary}'. In this last representation, "Coll" is not mandatory since there is only one dance (due to the fact that the existential quantifier for the dance is at the beginning of the sentence).
  Variables can be used within or just after the collection. Those prefixed by "@.?" are for the cumulative interpretation, those prefixed by "@_?" are for the collective interpretation, and those simply prefixed by '?' are for the distributive interpretation. E.g., in `{John, 1..* Female_person ?fp} ?p @.?ps', @.?ps refers to the collection itself while ?p is a universally quantified variable restricted to the members of @.?ps. Examples of use: `@.?ps has for size 10' and `?p has for type Person'. Note: "@.?" should NOT be confused with i) "@*?" (which prefixes sequence variables since in KIF '@' prefixes sequence variables), and ii) ".?" (which prefixes variables which do not have the default quantifier 'any' when they have no explicit quantifier, as noted in the definition of KR and in Section 0.4.1).

Some abbreviations (used in the first KRs below and re-used in all other KRs in this document):

• `>' is another identifier for the `subtype' relation type
  and FL allows its use in a KR as an abbreviation of "subtype:".
  However, `>' is not used in this document. Instead, `\.' is used: it is a subtype of `>' that also specify that the destinations are by default not exclusive nor complete. To specify that a subtype is a non-natural subtype, the abbreviation `\_' may be used. However, taking advantage of the fact that the subtype of a non-natural subtype is also a non-natural subtype, FL assumes that the use of `\.' abbreviates "natural_subtype" unless the destination is known to be a non-natural subtype.
  Similarly, `/^' abbreviates "supertype:" or, equivalently, "subtype of:".
  `<' and `>', which are respectively more common abbreviations for
  `supertype' and `subtype', can also be used in FL.
  However, the unbalanced use of the characters `<' and `>' in a text/HTML file
  leads most text editors not to check and show anymore the balancing of parenthesis, brackets, ...
  unless a special configuration is set. Since this balancing check and display is very useful for
  designing KRs, the author of this document (and creator of FL) most often uses abbreviations that
  do not include the characters `<' and `>'.
  `\.' and `/^' have been chosen because they are short and not-too-conspicuous combinations of
  ASCII-based letters that respectively look like '↘' and '↗'. Indeed, graphically, the supertype and
  subtype relations are generally respectively represented via upward and downward arrows.
  The other abbreviations usable in FL have similar rationale.
• `==' abbreviates `equal', `<=>' abbreviates `equivalent' and '=' abbreviates `equal_or_equivalent'.
  When a relation `=' is used between two types, it implies that the subtypes and supertypes of one of the types are also subtype and supertypes of the other types.
  As for any other relation, this one is “according to the creator (and believers) of the relation”;
  hence, if a KB has KRs from various creators/believers, the user of an inference engine exploiting this KB must specify to the inference engine which believers it must take into account (this specification may be made within each query or via a command before queries).
• `\=' abbreviates specialization or `=' (and hence `subtype_or_equivalent').
• `:=' is another identifier for `full_definition':
  • If the destination is an expression (e.g. a function call), that "full definition" is an "equality by definition of the source term (the defined term)". Indeed, ":=" is the classic symbol for "equality by definition" and that meaning is kept in FL. If the destination expression is a function call, this expression is the body of the definition, not a function call which returns a definition. Unlike an equality, an equality by definition is not a symmetric relation. Because if is "by definition", this equality cannot be false: the term at source of that relation is simply defined to be whatever the creator of that relation has specified via the destination. If the destination is a contradiction, the term is defined to be a contradiction. However, in case of inconsistencies with the rest of the KB, there are two cases where such a definition cannot be inserted into the KB: i) when it is inconsistent with other usages of the term by the creator of the definition, and ii) when the defined term has been created by another creator (and hence includes an identifier of this creator). Section 1.3.9 precises these two cases and how they can be handed.
  • Otherwise, i.e. if the destination is a sentence, this one states a "necessary and sufficient condition" for being an instance of the source term and hence, at least if the definition is (semi-)formal, reuses a variable for this instance.
  • `:=' may also be used instead of ':' at the end of a relation node for specifying that the relation is necessary and sufficient for an instance of the source type to be of this type.
  • As specified (ex: in Section 0.4.3), subtypes of the relation type `definition' are
    `full_definition' (`:='), `sufficient_condition' (`:<=') and `necessary_condition' and `annotation'. The notes in the previous three points also apply to `:<=' and `:=>'.
  • A definition may be made
    - via an informal sentence (as in "any Entity is a Thing that is not a Situation"),
    - semi-formally (e.g. via an informal expression for the definition body
      as in `Entity := ^"Thing that is not a Situation"´), or
    - formally (as in `"Entity  exclusion:=> Situation"').
    The more formal, the better for reuse purposes.
• The following abbreviations are formally defined at the end of Section 0.3.3 and are very often used in the KRs below, although not the first time they could be used (this eases the understanding of the notions and, to that end, comments are also provided):
  • "p{ ... }" abbreviates "Subtypes_partition{ ... }" (wrt. the shared supertype of the subtypes in the partition) ; since in FL, the default interpretation of sets is distributive, [t1 \. p{t2, t3, t4}] relates t1 to its "subtype partition" composed of t2, t3 and t4.
  • "e{ ... }" abbreviates "Type_open_exclusion{ ... }", e.g. [t1 \. p{...}] relates t1 to an unclosed set of exclusive subtypes;
  • "c{ ... }" abbreviates "Closed_set{ ... }", e.g. [t1 \. c{...}] relates t1 to a closed|complete set of non-exclusive (but still different) subtypes;
  • "ne{ ... }" abbreviates Non-exclusive_set: it is usable for a set of things that is neither closed nor stating exclusion relation between its members (which still are different); this construct has the following advantages:
    - ensuring that its user has thought about whether or not
      the set is closed and the subtypes exclusive,
    - specifying different-from relations between the subtypes
      without a "unique name assumption" command,
    - grouping subtypes related to one criteria
      (and this one may be made explicit via a meta-statement on the set);
  • "part_p{ ... }" abbreviates "Parts_partition{ ... }" (wrt. the shared superpart of the things in the partition) which states that the set is closed and that the members have no shared part.
  • except for "ne", each of the above abbreviations may be prefixed by
    • "t_" (as in "t_p{...}") to indicate that what is stated is time_dependent, e.g. [Person \. t_p{Student Non-student}] specifies that a Student cannot be a Non-student but that it might at another time be a Non-student; thus, [Person \. t_p{Student Non-student}] is equivalent to [Person \_ t_p{Student Non-student}] (reminder: "\_" can be used for abbreviating non-natural_subtype);
    • "v_" (as in "v_p{...}") to indicate that what is stated is viewpoint_dependent, e.g. [Attribute \_ v_p{ Negative_attribute Positive_attribute }] and "Process \. v_p{ (Instantaneous_process = Event) Non-instantaneous_process }.

                                               abbreviation     converse        complement 
unary_relation-or-logic-operator    
  bivalent_not (\. closed-world_not)           ¬
  three-valued_not
    Kleene-and-Lukasiewicz (open-world_not)    !                ! 
binary_relation-or-logic-operator              
  converse //inverse (reverse)                 -                -
  exclusion    //[x =% !y], ![x y]             =>! =>.! =%.!    !-<=  !.%=      =>
    complement //[x <=> !y],functional excl.   =! <=>! <=>.!    !-<=>           <=>
  superior_or_equal //not "_or_equivalent"     =<               >               > //if same domain
    equal //_or_intensionally-equivalent-type  =                =               !=
      numerically_equal                        ==               ==              !=  !==
      identical-object_or_same-value-and-type  ===              ===             !== !=== 
  definition (":..." after a relation or not; any of the logic-specific_implication can be used)
    definition_by_intension (without '.' after the ':')
      definition_by_sufficient_condition       :<= :%= :<-      :->  :=% :only  
      definition_by_necessary_condition        :=> :=% :only    :<=  :%= :<- //only in the sense of NC     
        full_definition                        :=               :=
    //A definition can also be made via a definitional relation that is not subtype of "definition"
    // e.g. via its definition or because any (not every/each) is used in the source node.
    // By default, relations of type metalogic_deduction, supertype, equivalent_type
    //   or their inverses are "definitional by intension", while other relations are descriptive".
    //==== Conventions (overiddable by quantifiers) for NON-ABBREVIATED RELATION END DELIMITERS:
    // - ":=dc=" (or "must_dc ...:"): the relation is "descriptive for constraints" 
    //   (thus only for checking not assertion - e.g. sign. checking - but able to use all inferences);
    // - ":=pc=" (or "must_pc ...:"): the relation is "prescriptive for constraints"
    //   (only for checking purposes and not due to inferences, hence not able to use all inferences);
    //   Note1: alethic/deontic:  [some/no/each [...]  may/must be part of: this Universe];
    //          a parsing directive is an asserted constraint, and this one is a deontic sentence about
    //          relation in the current KB: [some/no/each &`...' may/must be part of this KB],
    //          e.g. [no/some Forward_declaration may be part of: this Module]
    //               !_! no Forward_declaration; ...; !_! each Forward_declaration is ok;
    //               module: the embedding [] or, if none, the current sentence (hence, till ';').
    //          // no "now" but "this Writing_time" (creation/update time != "this Reading_time")
    //   Note2: DOL specs define implications or other language element types in the current module
    //          wrt other language element types.
    //   Note3: for each hovered meaningful symbol (group), a contextual menu of relations for it can
    //          be generated (with some branches open to show the most important relations, in bold).
    // - ':' (not followed by an '=' or an arrow) at the end of the delimiter: 
    //       "descriptive (wrt./for inferences)" relation (this is the most usual case);
    // - '%-:' (possibly followed by an '=' or an arrow) to indicate ~"owl:InverseFunctionalProperty"
    //     e.g.: Woman child%-: a Thing;   Human id%-: a NoSS, an Id;   Human brain%-: 1 Brain';
    //     Note1: "owl:FunctionalProperty" = "at most 1" = "0..1". 
    //       \. owl#hasKey // https://www.w3.org/TR/owl2-syntax/#Keys  TR/owl2-new-features/#F9:_Keys
    //     Note2: "UML composition", e.g. `every House<-.: some House //no more House => no more Room
    //            (!dependency)      but  `every Bike  part: 2 wheel' //no more Bike, still the Wheels
    // - "100%=>", "100%=" or "100%<=" (not '.': "this type") at the end of the delimiter: 
    //   the relation is a "subtype/equivalence definition by extension"
    //   (add 'D' begore '@' for "Default");
    //   in extensional supertype/subtype relations, the least specialized part is the one defined;
    //   in intensional supertype/subtype relations, the most specialized part is the one defined;
    // - otherwise (ending by ":="/":<="/":=>", or ":—"/":%—"/":—%", or ...):
    //   "definition by intension" (below, the abbreviations BEGINNING by ":" or "|" are
    //    "definitional by intension"; however, even though supertype/subtype relations
    //    and equivalent_type relations are by default "definitional by intension", some of their
    //    abbreviations in the rest of the table do not have such an ending/beginning or beginning)
    //    Note1: _[(Default)every/any/8%|each->...]: ":D*=>" / ":->" / "atLeast8%=>"
    //    Note2: Bull_shark.(?s) :(.|@|100%|+86%<-  //here '.' ok too since no ambiguity
    //                                  [?s type:Shark,part:(a Pectoral_fin shape:a Triangle)].
    //==== Conventions for symbols in RELATION ABBREVIATIONS:
    // - arrow: -  descr./def. prefix: '' for descr, ':' for non-descr (e.g. def.); '-' if unknown
    //                                               ':.' for an extensional defin.  
    //            //old: (description <=> Embedded-sentence_assertion: [?p .=> ?p2] <=> [.?p => ?p2];
    //             for def.: (default/8%)every/any/each via ":D*->" / ":->" / ":D+8%->"|":D@->")
    //          - never "!<-": either "!-<-" (excl) or "! <-": `x !-<-y ' <=> `y ->! x' <=> `y -> !x'
    //            note: "x <- y" (y: proof of x with more info) better than "x <=> y" (y paraphrases x)
    //          - "c" on the side of the corrected sentence
    //          - dir: instead of '<' or '>', '|' used for metalogical stuff, otherwise '%' is usable;
    //                 doubling '<'/'>'/'%' indicates mono-directionality-only
    //          - dash: '—' but '~' for "non-fully logic"; repl/add '=' if eq.included
    //                  doubling '~'/'-'/'=' means "without gen.-or-spec"
    // - gen.:  - dash: doubling '_' means "without implic.-or-concl."
    //          - direc: '^'/'.';  if indiv. involved: '..' used on  the individual side
    //          - andArrows: arrow added before or after;  orEq: '=' added before or after 
    //          - '@': for a subtyping/equivalence by extension.
  positive_gradual-rule_destination            ++/^  ++:        ^\++:  ++:   //+: --/^ --:, ^\-- 
  negative_gradual-rule_destination            +-/^  +-:        ^\-+   -+:   //+: -+/^ -+:, ^\+- 
  output_or_successor_or_implication           --*   */^
    general_implication_from_a_phrase          **=>             <=**  
      metalogic_deduction                      
        syntactic_deduction                    |-  ⊢  ⊢         -| 
          syntactic_equivalence                |<->             |<->
        semantic_deduction                     |=  ⊧
          semantic_equivalence                 |<=>             |<=>
      logic-specific_implication               *=>              <=*  
        //reminder: begin by ':' if defin, then by '.'/10% if by extension (or by '-' if unknown)
        logicalImplicByIntOrExt                =>               <=              =>!  =>.!  
          ..._and_generalisation               =>/^  /^=>       <=\_  \_<=    
          ..._and_generalisation_by_extension  100%=>/^         100%<=\_        
        rule (defin with ':' 1st)              ~>               <~=             ~>!   ~>.!
          //reminder: "<~" rules (e.g. Prolog rules ":-") express "sufficient" conditions! 
          ...wo.gen.-or-spec.                  ~~>              <~~=            ~~>! ~~>.!
          ..._and_generalisation               ~>/^   /^~>      <~=\_           
        logical/rule_descriptive_implication   =>   ~|>         <=  <|~        =>! =>! =>.!
          modus-ponens-only_descr-implic       =>>  ~|>>        <<= <<|~   
          descriptive_material_implication     =>|             |<=
          descriptive_formal_equivalence       <=>             <=>            <=>!  <=>.!
  semantic_gGeneralization_or_equivalent                                        =!
    core-generalization_or_equivalent          =/^                 ^\=  \=
      equivalent //see below for strict gen.   =*               =*              =!            
        intensionally_equivalent_type          =                =               =!  
        extensionally_equivalent_type          .=               .=              =!  
        //eq_between_phrases: see above 3 equivalence cases
    semantic_strict_gGeneralization           */^               =^\*            =! 
      type                                     |^               =|.
      semantic_core-strict-generalization      /°               =°\  °\=
        super_individual                     ../^  ../          =\.. ^\..=
        supertype                              /^   <           =\.  ^\=  >= 
          natural-type_supertype              _/^               =\_
          non-natural-type_supertype          ~/^               =\~   \~=  
          extensional_supertype               ./^              .=\.  .\=
        phrase_strict-generalization         ._/^  ._/          =\_.  \_.=      =! 
          phrase_gen._wo._implic.-or-concl   __/^  __/          =\__ ^\__=   
          phrase_implication_and_generalization: see above "..._and_generalisation" cases
  corrective_relation                        c-binaryRelAbbrev  binaryRelAbbrev-c

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Input
"check level "{NUMERAL}";"        PtKkIn->doAllChecks

========== Parsing

---------- module:
!_! no/do Module_reloading;     // !_! each Module_reloading is mandatory;
  // !_! each ^(Loading_instruction parameter: a Module ?m) trigger of: (a Loading  input: ?m)

---------- declaration:
!_! no/allow Forward_declaration; //disallow Forward_declaration !_!each Forward_declaration is allowed
  !_! no/allow Link_forward-declaration;
  !_! no/allow Declaration_via_descriptive relation;


---------- lexical:
unprefixed variables; prefixed variables;  PtKoIn->areVarValuesLikeIdentifiers=true
"unprefixed terms are key names;" {if(Run)PtKkIn->isUnprefixedIdentsAllowed=true;}
"unprefixed identifiers allowed;" {if(Run)PtKkIn->isUnprefixedIdentsAllowed=true;}
"no unprefixed identifiers;"      {if(Run)PtKkIn->isUnprefixedIdentsAllowed=false;}
"use names;" "no names;"          {PtKkIn->areNamesAllowed=true;}
"ambiguityAcceptation "{NUMERAL}";" &PtKkIn->bAmbiguityAcceptation);=
!_! `this User'_._set("pm","pwd"); //or gets password, or = pm/null;  ? this User
!_! default Source/Creator/Interpreter := ...

---------- structural:
"no exclusion check;"
"\"incorrect kind\" errors;"      {PtKkIn->noIncorrectKindErrors=false;}
"no exitAtError;"                 PtKb->oErr.nbErrorsToReachForExiting=0;
allow types of relations on relations;" PtKkIn->areTypesOfRelationOnRelationAllowed=true;


========== Command
"gets;" 



@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Output

========== During parsing
"run mode;" "load mode;" "display mode;"   "include/load/display/run/output/format "{IDENT}";" 


========== During execution
"no reasoning trace;"          PtKb->oTrace.nReasoningTraceLevel= 0;PtKb->oTrace.nTraceLevel

========== Command
echo|print   "map"



@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Execution (updates, calls, ...)

========== Directive
"no storage;"

========== Command
exit del mod  "e-mail"   "date;"  "duration;"  "sleep "{NUMERAL}";"





OMS
  \. (dol#model = System_repr,
       != (logic#model = (dol#realization != uml#realization, 
                           = "semantic interpretation of all non-logical symbols of a signature") ) ),
  p: (dol{logical_theory
       \. ontology = "explicit and shared formal representation of the entities and ...",
       p: sentences  (signature p: 1..* (dol#Non-logical=symbol = cl#names (cl#sequence=marker = list),
                                          \. individual class property ) )
     )                                   //denoting an object from the domain of discourse

p35: http://www.thezfiles.co.za/ROMULUS/home.html
p142: sublanguageOf, ...
p150: A formal representation of language and logic translations still needs to be developed
      see QVT or [7] (LATIN short paper; see my own references)
p181: HETS, Ontohub, Modelhub, Spechub, ...    API4KP.