KIF functions/relations to handle lexical and semantic contextualization (beliefs, preferences, ...)

Dr Ph. MARTIN
Mostly created in February 2012;   last updated in December 2012.

More explanations on "shared KB core model" supported by the functions/relations below
are in (yet unpublished) Section 2 of this other article
(because of space constraints, this other article was finally submitted and published without its Section 2;
this Section 2 will thus be the subject of a separate article)

This file contains some KIF functions/relations which, if they are used by people to make definitions and assertions, permit a knowledge base (KB) to include these statements (without using modules) and be consistent even though its statements come from different sources (files or agents) and hence can contradict each other. More precisely, these functions and relations ease and handle the specification of terms and statements contextualized by their sources.

For the KB to be consistent without using modules, every term defined/declared by one of the sources - i.e., every term that is not a term predefined in KIF - should be lexical contextualized by their sources, that is, prefixed (or postfixed) by an identifier of its source, as in http://url_identifying_the_source#term_identifier_in_the_source_namespace or xsd:float (with the XML namespace shortcut). Since ':' and '#' already have special meanings in KIF, '%' is here chosen for the ending of the source prefix in a term. Postfixes are not yet handled.

For the KB to be consistent without using modules, every "belief" - i.e., every statement that is not a definition nor a command - should have a (semantic) context that specifies its source. (This is not needed for definitions since the source is lexically specified via the defined term). Statements can be put in different modules but their sources still need to be represented. The direct use of meta-statements is more flexible. A meta-statement contextualizes a statement if it adds "contextualizing relations" to it, that is, constraints without which the statement is or may be false. may be false, e.g., "belief source" relations and temporal/modal relations.

The KIF representation below are in the courier font and are enclosed within the XHTML marks <KR> and </KR> to permit a parser to distinguish them from regular text. KIF is a LISP-based relatively intuitive first-order-logic language that became popular for formalizing and translating knowledge representation languages (KRLs) and ontologies. The KIF syntax used below is the one of KIF 3.0 plus the new constructs introduced by dpANS KIF. The model and syntax of KIF (Knowledge Interchange Format) were respectively mostly re-used by the Common Logic standard and its CLIF notation but without the KIF features for specifying meta-statements, definitions and (monotonic or not) inference rules. First-order statements and some 2nd-order-looking ones can be expressed in KIF. Thus, all statements that can be expressed with the W3C KRLs (OWL+ RDF/XML, N3, RIF, ...) can be expressed in KIF and in this model.

Except for operators (pm%def_rel, ...), all identifiers are nominal expressions (this is a best practice). For a "concept type" ("unary relation" in KIF, "class" in RDF), the initial is in uppercase. For a "relation type" ("function" or "non-unary relation" in KIF, instance of rdf:Property if it is binary), the initial is in lowercase. Variable names begin by '?'. Terms without prefix are KIF terms. "pm%" is the prefix for terms created by the author of this article.


Table of contents
1.  Checking statements specified with the constructs of Section 2
2.  Specifying a belief/definition and its main source (agent or file)
3.  Contextualizing terms (i.e., avoiding lexical inconsistencies)
4.  Contextualizing statements (i.e., avoiding statement inconsistenties)
5.  Choosing between other agents' contradictory beliefs (contextualized statements)
6.  Handling sets, lists and strings
Annexes. A1.  For programmers: top-level of an object-oriented model


1.  Checking statements specified with the constructs of Section 2

During the parsing of a new statement, knowing its asserter and the date, the
KBMS (KB management system) should call the next defined function on this statement
to check it with respect to (wrt) the KBMS policy and the criteria selected by the
(end-)user. If the checks are ok, the statement is inserted into the KB.

The statement must specify its source contextualizations. An easy way to do so is to
use an operator such as pm%def_fct, pm%def_rel and pm%belief_from (see Section 2),
or any subtype of pm%source (see section 2).

(pm%def_fct pm%assertion_by (?asserter ?assertion_date ?belief_or_def)
                                 :-> ?assertion  :=>
  ;;pm%def_fct defines a functional relation (if the relation is binary, it is an
  ;; instance of owl:FunctionalProperty and the function is unary); 
  ;;pm%def_fct returns nil if no assertion
  (exists ((?dated_assertion) (?is_assertable))
    (and (= ?dated_assertion                                   
            (if (not (pm%valid_statement ?belief_or_def))  nil   
             (if (or (= ?assertion_date nil)                    
                     (pm%Definition ?belief_or_def) )  ?belief_or_def
              (listof ^(pm%assertion_date ,?belief_or_def ,?assertion_date))
             )))
         (= ?is_assertable                                      
            (and  (/=  ?dated_assertion  nil)                    
                  (forall ((?list_of_bad_kinds_of_statement) (?bad_kind_of_statement))
                    (and (pm%kinds_of_statement_this_agent_has_committed_not_to_assert
                                             ?asserter ?list_of_bad_kinds_of_statement)
                         (item ?list_of_bad_kinds_of_statement ?bad_kind_of_statement)
                         (not (holds ?bad_kind_of_statement ?dated_assertion )) ))))
                             ;;holds must be used when the predicate/rel. is a variable
         (=> ?is_assertable  (and (= ?asserted_belief  ?dated_assertion)
                                  (wtr ?dated_assertion) ))       
                                 ;;wtr: weakly true (asserts if no paradox created)  
         (=  ?assertion (if (not ?is_assertable)  nil  ?dated_assertion)) 
    )))

  (pm%def_rel pm%kinds_of_statement_this_agent_has_committed_not_to_assert (?agent ?list)
    :=> ;;this is a partial definition (it may be completed later if needed)
    ;;e.g.,  (pm%kinds_of_statement_this_agent_has_committed_not_to_assert pm
    ;;          (listof pm%Belief_implicitly_contradicting_another_one) )
    (and (pm%agent ?agent) (list ?list)) )

  (pm%def_fct pm%valid_statement (?belief_or_def)  := ;;complete definition
    (if (pm%Assertion_of_statement_source ?belief_or_def) true
     (if (pm%Definition ?belief_or_def) false  true) ))

    (pm%def_rel pm%Assertion_of_statement_source (?statement) := 
      (exists ((?r) (?source))
        (and (= ?r (first ?statement))
             (or (and (pm%subtype_or_equal pm%source ?r)  ;;last argument: the source
                      (pm%valid_belief_for_that_source (last ?statement)
                                                       (pm%second ?statement) ))
                 (and (pm%subtype_or_equal pm%source_of ?r)
                      (pm%valid_belief_for_that_source (pm%second ?statement)
                                                            (last ?statement) )) ))))

      (pm%def_rel pm%valid_belief_for_that_source  (?source ?statement) :=
        (exists ((?source2))
          (or (sentence ?statement)
              (and (pm%Def_statement ?statement)  (/= ?source2 ?source)
                   (pm%term_source_from_lexical_viewpoint (pm%second ?statement) ?source2)
              ))))

    (pm%def_rel pm%Definition (?statement) :=
      (exists ((@defRest))
         (or (pm%Def_statement ?statement)  //definitions via pm%def_rel or pm%def_fct
             (= ?statement ^(defrelation pm%def_rel @defRest)) ;;+ the def. of pm%def_rel
         )))  //and the def. of pm%def_rel
         
      (pm%def_rel pm%Def_statement (?statement) :=
        (exists ((?def_op))
          (and (= ?def_op (first ?statement)) 
               (or (= ?def_op pm%def_rel) (= ?def_op pm%def_fct_rel)
                   (= ?def_op pm%def_fct) ))))


2.  Specifying a belief/definition and its main source (agent or file)

(pm%def_rel pm%source_of (?source @args) :=  ;;when a binary relation with a name ending 
  ;;by "_of" is defined via pm%def_rel, this operator also generates the inverse relation
  ;;by taking off "_off"; however, since pm%source_of is not binary, it has to be defined
  (forall ((?arg))
    (=> (pm%item (listof @args) ?arg)  (pm%source ?arg ?source)) ))

(pm%def_rel pm%source (?object ?source) :=>   ;;object: term or statement
  ;;e.g., (pm%source '(pm%correction oc%all_birds_fly
  ;;                                 oc%in_2012_at_least_75pc_of_Aussie_birds_can_fly) oc)
  ;;any sub-statement of ?statement has for source ?source
  (and (=> (pm%file  ?source) (pm%source_file  ?statement ?source))
       (=> (pm%agent ?source) (pm%source_agent ?statement ?source))
       (pm%subtype_according_to pm pm%source ;;some of its subtypes according to pm are:
                    pm%source_file pm%source_agent pm%contextualizing_source)
       (=> (sentence ?object)
           (and (pm%contextualizing_source ?object ?source)
                (=> (pm%agent ?source) (pm%believer ?object ?source)) ))
                ;;above line: any ?object has for pm%believer its source
       (forall ((?substatement)) (=> (pm%substatement ?statement ?sub-statement)
                                     (pm%source ?sub-statement ?source) ))))

  (pm%def_rel pm%believer (?sentence ?believer) :=>
    (and (pm%believer_of ?believer ?sentence)
         (pm%supertype_according_to pm pm%believer ;;some supertypes according to pm are:
                                       pm%contextualizing_source pm%source_agent ) ))

    (pm%def_rel pm%believer_of (?believer @sentences) :=>
      (and (pm%Agent ?believer)
           (forall ((?se)) (=> (pm%item (listof @sentences) ?se)
                               (pm%believer ?se ?believer) ))
           (pm%subtype_according_to pm pm%Contextualizing_relation pm%believer) ))

(pm%def_rel pm%named_belief (?term ?belief) :=
  ;;e.g., (pm%named_belief  oc%all_birds_fly  
  ;;        '(forall ((?b pm%bird)) (exists ((?f pm%flight)) (pm%agent ?f ?b)) ) 
  (exists ((?source source))
    (and (= term ?belief)
         (pm%if_this_term_has_a_source_then_this_sentence_has_the_same  ;;see Section 3
                                                 ?term ?source ?belief ))))

(pm%def_rel pm%def_fct (?relTerm ?args ?defSymbol @defBody) := 
  (exists ((?source source) (?relDef))
    (and (pm%symbol_for_conservative_definition ?defSymbol @defBody)
         (= ?relDef ^(deffunction ,?relTerm ,?args ,?defSymbol ,@defBody))
         (wtr ?reldef)  ;;assertion of the definition 
         (pm%if_this_term_has_a_source_then_this_sentence_has_the_same 
                                              ?relTerm ?source ?relDef ))))

  (pm%def_rel pm%symbol_for_conservative_definition (?symbol @defBody) :=
    (exists ((?defSymbol)) ;;symbol cannot be tested directly (see next line)
      (and (= ?defSymbol
              (if (/= ?symbol ':->)  ?symbol  (first (rest (listof @defBody))) )
           (or (= (?defSymbol ':=)) (= (?defSymbol ':<=)) (= (?defSymbol ':=>))) )))

  ;;pm%def_fct_rel permits to define and use a "term" as both a relation and a function
  ;; (the last parameter of the relation is the result of the function);
  ;;more precisely, since in KIF functions and relations are in different namespaces,
  ;;  pm%def_fct_rel generates a function definition which has the same "name" as the
  ;;  relation and is simply a call to this relation; the KIF parser distinguishes
  ;;  between these two different objects according to their number of parameter and
  ;;  the way they are called;
  ;;KIF proposes the form "deffunction constant (vars) :-> indvar :<= sentence"
  ;;  but not the form    "deffunction constant (vars) :-> indvar :=  sentence"
  ;;  pm%def_fct_rel permits something equivalent to the last form:
  ;;                      "pm%def_fct_rel constant (vars) /*:->*/ indvar :=  sentence"
  ;;this next definition body uses 2 free variables as implicitly quantified variables;
  ;;this is the only place in this file but this is common in the KIF documentation, e.g.,
  ;;  (deffunction first (?l) := (if (= (listof ?x @items) ?l) ?x))
(pm%def_rel pm%def_fct_rel (?relTerm ?args ?defSymbol @defBody) := 
  (and (= ?defSymbol ':=')
       (pm%def_rel ?relTerm ?args ?defSymbol @defBody)
       (pm%def_fct ?relTerm (butlast ?args) ':=
          ^(if (and (= ,?args (listof @fct_args ?result)) ;;the last 2 variables are free
                    (,?relterm ?fct_args) )  ?result
            bottom ))))

(defrelation pm%def_rel (?relTerm ?args ?defSymbol @defBody) := 
  ;;conservative definition (unique (within namespace) and <=>/<=/=> based) 
  ;;   => no inconsistencies added when definition added (not CALLED)
  ;;e.g., (pm%def_rel pm%car (?car) := (pm%entity ?car))
  (exists ((?source source) (?relDef))
    (and (= ?relDef ^(defrelation ,?relTerm ,?args ,?defSymbol ,@defBody))
         (pm%symbol_for_conservative_definition ?defSymbol @defBody)
         (wtr ?reldef)  ;;assertion of the definition 
         (pm%if_this_term_has_a_source_then_this_sentence_has_the_same
                                                                ?relTerm ?source ?relDef)
         (pm%if_this_relTerm_has_an_inverse_then_it_has_the_same_source ?relTerm ?source)
     )))
(pm%source pm%def_rel pm)

(pm%def_rel pm%supertype (?type ?supertype) :=
  (forall ((?instance)) (=> (holds ?type ?instance) (holds ?supertype ?instance))) )

(pm%def_rel pm%supertype_according_to (?source ?type ?supertype) :=
  (exists ((?source))
    (and (=> (not (term ?type)) ;;?type must be defined
             (and (term ?supertype) ;;the supertype must exist
                  (pm%term_source_from_lexical_viewpoint ?type ?source) ;checking
                  (wtr ^(pm%def_rel ,?type (?t) :=> (pm%supertype ?t ,?supertype))) ))
         (=> (term ?type)
             (and (=> (not (term ?supertype))  ;;?supertype must be defined
                      (and (pm%term_source_from_lexical_viewpoint ?supertype ?source)
                           (wtr ^(pm%def_rel ,?supertype (?t) :=>
                                     (pm%supertype ,?type ?t) ))))
                  (=> (term ?supertype)
                      (or (pm%supertype ,?type ?supertype)
                          (=> (pm%term_source_from_lexical_viewpoint ?type ?source)
                              (wtr ^(pm%def_rel ,?type (?t) :=>
                                       (pm%supertype ?t ,?supertype) )))
                          (=> (pm%term_source_from_lexical_viewpoint ?supertype ?source)
                              (wtr ^(pm%def_rel ,?supertype (?t) :=>
                                       (pm%supertype ,?type ?t) )))
                          (=>> (consis (pm%supertype ?type ?supertype))
                               (source '(pm%supertype ?type ?supertype) ?source) )
                      )))) )))

(pm%def_rel pm%subtype_according_to (?source ?type ?subtype) :=
  (pm%supertype_according_to (?source ?type ?subtype) )

  ;;KIF permits to represent "default rules" (and thereby non-monotonicity and the
  ;;"closed world assumption") via the use of "=>>" (instead of "=>") and 
  ;;"(consis ?s)" which means "as long as ?s is consistent with the current rest of the KB"
(pm%def_rel pm%default_truth (?sentence)  :=
  (wtr ^(=>> (consis ,?sentence) ,?sentence)) )


3.  Contextualizing terms (i.e., avoiding lexical inconsistencies)

(pm%def_rel pm%if_this_term_has_a_source_then_this_sentence_has_the_same 
            (?term ?source ?sentence) :=
  (=> (pm%term_source_from_lexical_viewpoint ?term ?source)
      (and (pm%source ?term ?source) (pm%source ?sentence ?source) (wtr ?sentence)) ))
 
  (pm%def_rel pm%term_source_from_lexical_viewpoint (?term ?source) :=
    (exists ((?sourceName string) (?category))
      (and (= ?sourceName (pm%term-name_source (name ?term)))
           (=> (pm%category_identifier ?category ?sourceName) (= ?source ?category))
           (=> (not (pm%category_identifier ?category ?sourceName))
               (= ?source ?sourceName) )
           (pm%source ?term ?source) )))

  (pm%def_fct pm%term-name_source (?termName) := 
    ;;e.g., (pm%term-name_source "aSource%stuff") -> "aSource"
    (exists ((?beforePercent string) (?afterPercent string))
      (if (= (name ?term) (append ?beforePercent (append "%" ?afterPercent)))
         ?beforePercent
        nil )))

(pm%def_rel pm%if_this_relTerm_has_an_inverse_then_it_has_the_same_source 
            (?relTerm ?source) :=
  (exists ((?s string) (?inv binary_relation))
    (=> (= (name ?relTerm) (append ?s "_of"))  ;;if ?relTerm = ?s + "_of"
        (=> (binary_relation ?relTerm)
            (and (name ?inv ?s)
                 (pm%if_this_term_has_a_source_then_this_sentence_has_the_same 
                             ?inv ?source ^(pm%inverse (inverse ,?term) ,?inv) )) ))))


4.  Contextualizing statements (i.e., avoiding statement inconsistenties)

(pm%def_rel pm%uppermost_context (?statement ?context) := 
  (and (pm%substatement ?context ?statement) (pm%uppermost_contexts ?context nil)) )

(pm%def_fct_rel pm%uppermost_contexts (?statement /*:->*/ ?contexts) := 
  (and (= ?subs (pm%substatements ?statement))
       (= ?contexts (pm%map_less_nil_and_duplicates
                      (lambda (?x) (pm%uppermost_contexts ?x))  ?subs) )))


(pm%def_rel pm%metastatement (?statement ?metastatement) :=  ;;direct or not
  (pm%substatement ?metastatement ?statement) )

(pm%def_rel pm%substatement (?statement ?subStatement) :=  ;;direct or not
  (and (sentence ?statement)  (sentence ?metastatement)
       (pm%item (pm%sub_statements ?statement) ?sub-statement) ))

(pm%def_fct pm%substatements (?statement) := 
  ;;-> list of statements containing no "and" 
  (if (not (list ?statement))  (listof ?statement)
   (if (= 'and (first ?statement))
      (append (listof ?statement)
              (map pm%atomic_substatements (rest ?statement)))
    (append (listof ?statement)
            (map first (map pm%atomic_substatements ?statement)) ))))


(pm%def_rel pm%atomic_substatement
            (/*1..*/?statement /*1..*/?atomicSubstatement) :=
  (pm%item (pm%atomic_substatements ?statement) ?atomicSubstatement) )

  ;;the top function for dividing a statement into its "atomic substatements",
  ;;i.e., statements that cannot be divided into "contextualized AND-clauses"
  ;;(indeed, no (sub-)statement should be handled without its contextualization):
(pm%def_fct pm%atomic_substatements (?statement) := 
;;-> list of substatements containing no "and"; examples:
;;1. (pm%atomic_substatement '(believer_of pm '(and ?as1 (time_of 2012 (and ?as2 ?as3)))))
;;                       ->  '(believer_of pm '?as1)
;;2. (pm%atomic_substatement '(believer_of pm '(and ?as1 (time_of 2012 (and ?as2 ?as3)))))
;;                       ->  '(believer_of pm '(time_of 2012 '?as2))
;;3. (pm%atomic_substatement '(believer_of pm '(and ?as1 (time_of 2012 (and ?as2 ?as3)))))
;;                       ->  '(believer_of pm '(time_of 2012 '?as3))
  (if (not (list ?statement))  (listof ?statement)
   (if (= 'and (first ?statement))  (map pm%atomic_substatements (rest ?statement))
    (if (pm%Non_contextualizing_relation_on_a_sentence (first ?statement))
        (append (listof ?statement) (map first (map pm%atomic_substatements ?statement)))
     (map first (map pm%atomic_substatements ?statement)) ))))


(pm%def_rel pm%Non_contextualizing_relation_on_a_sentence (?r) := 
  (and (pm%Non_contextualizing_relation ?r) (pm%Relation_on_a_sentence ?r)) )

(pm%def_rel pm%Non_contextualizing_relation (?r) := 
  (and (relation ?r) (not (pm%Contextualizing_relation ?r))) )

(pm%def_rel pm%Contextualizing_relation (?r) :=
  (and (relation ?r)  ;;actually (pm%Relation_on_a_sentence ?r) but this is redundant here
       (forall ((@args)(?se))
          (and (=> (holds ?r @args)
                   (exists ((?s sentence)) (and (pm%item (listof @args) ?s)
                                                (wtr ?s) )))) )))

(pm%def_rel pm%Relation_on_a_sentence (?r) := 
  (and (relation ?r)
       (forall ((@args)(?se))
          (=> (holds ?r @args) 
              (exists ((?s sentence)) (pm%item (listof @args) ?s)) ))))


5.  Choosing between other agents' contradictory beliefs (contextualized statements)

(pm%def_rel pm%End-user (?user)  :=>  (pm%Agent ?user))  ;;an end-user is an agent
   ;;when an agent enter a statement, import a file or issue a commend, the KBMS can 
   ;; make its identifier an instance of pm%End-user

  ;;the next statement specifies that by default every belief of the end-user is true
  ;;(this is a way for the KBMS to start making inferences on the beliefs of the end-user
  ;; by stating that they are true without their contextualization by their source):
(forall ((?a pm%agent))
  (=> (pm%End-user ?a)
      (pm%default_truth  ^(forall ((?s)) (=> (pm%believer ?s ?a) (wtr ?s)))) ))

  ;;a relation to test the non-contradiction of a user's beliefs:
(pm%def_rel pm%Believer_of_a_consistent_set_of_beliefs (?agent) :=
  (consis (forall ((?s sentence)) (=> (pm%believer ?s ?agent) (wtr ?s)))) )


  ;;a credulous agent believes anything as long as he has no reason not to
(pm%def_rel pm%credulous (?agent)  := 
  (forall ((?s)) (pm%default_truth ^(pm%believer (pm%atomic_substatements ,?s) ,?agent))) )

  ;;all agents are credulous by default (an example rule for a KBMS policy):
(forall ((?agent pm%agent)) (pm%default_truth ^(pm%credulous ,?agent)))


  ;;by default, when an agent appears to believe in pm%correction relations between statements,
  ;;he believes only the most corrected statement:
(forall ((?a pm%agent)  (pm%default_truth ^(pm%believer_of_the_most_corrected_version ,?a) ) )

  (pm%def_rel pm%believer_of_the_most_corrected_version (?agent)  :=
    (forall ((?s1) (?s2))  (pm%default_truth
      (and (pm%believer ^(pm%correction ,?s1 ,?s2) ,?agent)
           (not (pm%believer ,?s1 ,?agent)) 
           (pm%believer ?s2 ,?agent) )))) ;;thus, if there is a hierarchy of corrections,
                                          ;;only the most corrected is finally believed by the agent


(pm%def_rel pm%Statement_implicitly_contradicting_another_one (?s) :=  ;;was no_other bef06/2013
  (pm%Belief_implicitly_contradicting_another_one ?s) )
  ;;(conservative) definitions cannot contradict each other

(pm%def_rel pm%Conflicting_with_other_statements_of_the_KBs (?statement) :=
  (or (pm%At_least_partially_redundant_with_other_statements_of_the_KBs ?statement)
      (pm%Inconsistent_with_other_statements_of_the_KBs                 ?statement) ))

(pm%def_rel pm%Inconsistent_with_other_statements_of_the_KBs (?statement) :=
  (not (consis ?statement) ))

(pm%def_rel pm%implicit_specialization_and_not_instantiation (/*1..*/?s1 /*1..*/?s2) :=
  (and (<= ?s1 ?s2) (not (pm%instantiation ?s1 ?s2))) )

(pm%def_rel pm%specialization_and_not_instantiation (/*1..*/?s1 /*1..*/?s2) :=
  (and (<= ?s1 ?s2) (not (pm%instantiation ?s1 ?s2))) )

(pm%def_rel pm%instantiation (?s1 ?s2) :=  
  (exists ((@items)(?is2)(?t))
    (and (<= ?s1 ?s2)
         (or (= ?s2 (defobject @items))
             (and (pm%item ?s2 ?is2) (pm%instance ?t2 %i2)
                  (pm%direct_or_indirect_item ?s1 ?t2) )))) )


6.  Handling superior/better relations

(pm%def_rel pm%superior_for (?chrc ?o1 ?o2) := 
  ;;e.g.: (pm%superior_for precision RDF OWL)
  (forall ((?v1) (?v2)) (=> (and (holds ?chrc ?o1 ?v1) (holds ?chrc ?o2 ?v2))
                            (< ?v1 ?v2) )))

(forall ((?a pm%agent) (?chrc) (?o1) (?o2))
   (pm%default_truth  
     '(pm%believer '(=> (pm%superior_for ?chrc ?o1 ?o2)
                        (pm%better_for ?chrc ?o1 ?o2) 
                    )
                    ?a
      ) ))


(pm%def_rel pm%better_for_all_relations (?o1 ?o2) := 
  (forall ((?rel)) (pm%better_for ?rel ?o1 ?o2)) )

(forall ((?a pm%agent) (?chrc) (?o1) (?o2))
  (pm%default_truth '(=> (pm%better_for_all_relations ?o1 ?o2)
                         (pm%better ?o1 ?o2) )) )


7.  Handling sets, lists and strings

(pm%def_fct pm%cardinality (?set) :=
  (if (= ?set (setof @items))  (length (listof @items))  0) )

  ;;the relation 'item' and 'member' of KIF do not follow the common
  ;; graph reading convention (their arguments are in the wrong order);
  ;; pm%item and pm%member follow this convention
(pm%def_rel pm%member (?set ?member) :=  (member ?member ?set))


(pm%def_rel pm%item (?list ?item)  :=  (item ?item ?list))

(pm%def_rel pm%direct_or_indirect_item (?list ?item) := 
  (and (list ?l)  (not (null ?l))
       (or (= ?item (first ?l)) (pm%direct_or_indirect_item (first ?l) ?item)
                                (pm%direct_or_indirect_item ?list (rest ?l)) )))

(pm%def_fct pm%second (?list) :=
  (if (= ?list (listof ?x ?y @rest)) ?y bottom) )

(pm%def_fct pm%third (?list) :=
  (if (= ?list (listof ?x ?y ?z @rest)) ?z bottom) )

  ;;pm%map_less_nil is like 'map' but with 'append' instead of 'cons'
  ;;and hence without nil values
(pm%def_fct pm%map_less_nil (?fct ?list) :=
  (if (null ?list) (list)
   (append (value ?fct (first ?list))  (map ?fct (rest ?list))) ))

(pm%def_fct pm%map_less_nil_and_duplicates (?fct ?list) :=
  (pm%copy_less_duplicate_items (pm%map_less_nil ?fct ?list)) )

(pm%def_fct pm%copy_less_duplicate_items (?list) :=
  (if (null ?list)  nil
   (if (pm%item (first ?list) (rest ?list))  (pm%copy_less_duplicate_items (rest ?list))
    (cons (first ?list) (pm%copy_less_duplicate_items (rest ?list))) )))

(pm%def_rel pm%duplicate_item (?list ?x) :=
  (and (list ?list)  (not (null ?list))
       (or (and (= ?x (first ?list)) (pm%item (rest ?list) ?x))
           (pm%duplicate_item (rest ?list) ?x) )))


(pm%def_rel pm%String (?s) :=   ;;?s is a string iff it is a list composed of
                                ;; 0 or more characters
   (and  (list ?s)  (or (null ?s) (and (character (first ?s)) (string (rest ?l)))) ))



A1.  For programmers: top-level of an object-oriented model

class Objet : {/*...*/} ;
class ObjectReference : {/*...*/}; //pointer, database id, ...
class Quantifier : Object {/*...*/};

class Node : Object
{ RelationRefArray get_relationsOnThis (/*rel. selection parameters*/);//e.g., operatorOf,
  RelationRef      set_relationOnThis (/*rel. parameters*/);           //     parameterOf,
  //  references to relations connected (from/)to this node,           //        resultOf,
  //  directly or not ("directly" is a default in the parameters);     //   destinationOf,
  //1 relation selection parameter is the relation type: subtype,      //        sourceOf,
  //  type, creator, ... (a relation "creator" is (implicitly or       //meta-statementOf,
  //  not) about the node representation, not its semantic content)    //          partOf
  //A node that has a meta-statement (black/white context)
  //  has a relation of type pm#meta-statement (note: any node 
  //  that is existentially quantified (e.g., a relation) is a
  //  statement (and probably a sub-statement) and conversely ; 
  //  a statement is either a belief, definition or command (e.g.
  //  a query).
  //A (concept) node that is a meta-statement has a relation of 
  //  type pm#first_node and/or pm#embedded_node (an n-ary relation)
  //1 other parameter should allow the selection of binary
} //  relations that are "from"/"to" this node

class ConceptNode : Node  //alias, concept/frame/and-relation       //e.g., meta-statement,
{ //The code should not "know" that actually relations are stored   //operator, quantifier,
  //  in concepts, or concepts are stored in relations, or neither. //   parts, half_links
  //Similarly, the code should not "know" that node quantifiers 
  //  are stored in nodes or in relations: 
  QuantifierRef get_quantifier (/*rel. selection parameters*/);   
  QuantifierRef set_quantifier (/*rel. parameters*/);
  //A node that is a formal/informal "term" (e.g., a word, a type,
  //  a date, ...) has no/all quantifier(s).
  //A node that has a quantifier is not named (it is not a term).
  //A particular user is a term ; a set/class of users is not.
} //A node may have for creator/believer a (set of) user(s).

class RelationNode : Node   //alias, relation/function                  //e.g., operator,
{ //a relation has directly or indirectly related concepts              //    parameters,
  NodeRefArray get_relatedConcepts (/*concept selection parameters*/);  //        result
  NodeRef      set_relatedConcept  (/*concept parameters*/);
  QuantifierRefArray get_quantifiers (/*concept selection parameters*/);
  QuantifierRefArray set_quantifiers (/*concept selection parameters*/);
    //these are the quantifiers of the linked concepts;
}   //the existential quantifier of a relation is implicit