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

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 
                                              ?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 
                                                                ?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)))
        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)
                             ?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%believer '(=> (pm%superior_for ?chrc ?o1 ?o2)
                        (pm%better_for ?chrc ?o1 ?o2) 
      ) ))

(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

!-- ============= PPs-based decision making (1st version: 11-12/11/2016): //the decision/action related part of Logic-based cooperation // FOR EACH COOP APPROACH PARTITION, SHOW ADVANTAGES/DRAWBACKS OF EACH! // comm. (network, mail), // base (informalDoc(newsgrp):noRel, DB:type+part, alt-XML/JSON/no-SQL/wiki:+informalRel, KB // formal/informal stuff creation/enhancement/exploitation: // * indexation,alignment, normalisation, search,inferencing // * cooperation protocol / coop. rule/behavior enforcement: // - in physical/virtual BC building: alignment, replication // - task application (workflow, result/personne evaluation, decision) // e.g., a person that is is P-prooved uncooperative (e.g., does not // answer e-mail queries) is not eligible to any responsability // Note: publishing evaluations of person/site/product/... in an // organized normalized prooved way would already be good, // if only to vote/shop/coop/... // "people should vote" becomes "people should PP-log in a nexus" //See also coop_fr.html#idealCollaborativeTool including 5, e.g., "permettre à ses // utilisateurs de changer les règles par défaut de manière collaborative" Agent: an entity that can act. Set of rules, preferences and believed facts (SORPF) of an agent ?a: a set of statements (rules/preferences/facts) which ?a has explicitly declared that he follows/prefers/believes and that he wants to be judged by. Statements declared under duress are not valid. Logically conflicting statements in a SORPF do not count. The "rules of inference" of classical predicate logic (e.g., see are included by default but may be removed or complemented as long as this does not introduce nor remove internal contradiction in the rest of the principles nor means to detect any such internal contradiction. Formal/informal potential proof (PP) of a proposition ?p by an agent ?a: set of formal/informal inferences which, from hypothesis that ?a commits to believe (and that hence are added to his SORPF), lead to proove ?p, at least according to ?a. If the inference are formal, they must use inference rules in the SORPF of ?a the proof is not valid (i.e., it does not count as a PP) if an inference engine detects a problem in the application of the inference rules. No "argument", just "<=". Counter-"<=" are on premises or on false "<=" (e.g., "X has advantage A" => "X should be used"; correction: "X is better for A on any criteria than any other tool" => "X should be used") SORPFs-maximal-logically-coherent-union of SORPFs ?SORPFs of agents ?as: The "maximal logically coherent union" is a/the maximal part of the union that is logical coherent. If there are many possible maximal parts and if there are offendee ?os in ?as, the one(s) maximizing the number of rules from ?os should be used. If there are still more than 1 possible maximal part, random selection may be used. PP-based-addition by an agent ?a to a knowledge base ?kb: addition of statements to ?kb which, when they contradict other statements in ?kb, must be supported by a valid PP and, if so, replace them. SORPFs-betterment of a proposition ?p1 by a proposition ?p2 w.r.t. SORPFs ?SORPFs: for all ?a in ?as, according to his SORPF (preferences and conclusions from them via the rules of the SORPF), ?p2 is better than ?p1 (each SORPF may define different rules for calculating what "better" means). Note: there may often not be enough information in a SORPF to conclude that ?p2 is better than ?p1 for this SORPF; in that case, the agent with this SORPF may be asked to complete it. SORPFs-majoritarily-betterment of a proposition ?p1 by a proposition ?p2 w.r.t. SORPFs ?SORPFs: for more than 50% of all ?a in ?as, according to his SORPF, ?p2 is better than ?p1. //better includes more true/general SORPFs-majoritarily-invalidation of a proposition ?p1 by a PP ?pp w.r.t. SORPFs ?SORPFs (or agents): in at least one SORPF in ?SORPFs, there is a fact which w.r.t. the rules of at least one SORPF in ?SORPFs, contradicts ?p1 and this contradiction ?pp is not SORPFs-majoritarily-invalidated by more than 50% of the ?SORPFs ?s (note1: by default, in any SORPF, the following notion is inserted: if a part of a proposition/thing that is not an OR is proven false/fake, this proposition/thing is invalidated; note2: since there may often not be enough information in a SORPF to make the above cited inference, the agents owning the SORPF may be asked to complete them). SORPFs-majoritary-invalidation-or-betterment of a proposition ?p1 by a proposition ?p2, w.r.t. SORPFs ?SORPFs: SORPFs-majoritary-invalidation of ?p1 by ?p2 w.r.t. ?SORPFs, or SORPFs-majoritary-betterment of ?p1 by ?p2 w.r.t. ?SORPFs. SORPFs-majoritarily-approval of a proposition ?p1 w.r.t. the SORPFs ?SORPFs of agents ?as: ?p1 is not SORPFs-majoritarily-invalidated by ?SORPFs and there is no ?p2 from one of the ?as that is a SORPFs-betterment of ?p1 wrt ?SORPFs. R1: Any agent who does not declare his principles may be assumed to have none. R2: Anyone may complement/correct his SORPF by PP-based-additions (no genuine removal is allowed but some privacy setting may be used). The rule "changes are allowed" is then also automatically added and canot be removed. R3: In case of a conflict ?c between entities ?e1 ... ?en, they are judged according to the SORPFs-maximal-logically-coherent-union of their SORFs at the time of ?c (including the statements implicitly adhered to, e.g., rules of the land where ?c occured). R4: rules/decisions must have PP for each of their category restrictions (e.g., why for this man and not to any, men and not human, why human and not animal, ...) R5: //implem/formaliz of "do not do to other what you would not like others to do to you", // "do what they majoritarily do not want you to do to them", // "deciders must take rational decisions for the average optimal benefit of all" // "deciders must be able to explain the decisions, must not abuse their powers, ...", // "no dictature of some individuals nor of the ignorant majority", ... An entity ?e is allowed to perform an act ?act (e.g., make a decision, change the cooperation rules), that affects other agents ?as (in the sense of entities that can act to avoid consequences of ?act) ONLY IF 1) he offers ?as the opportunity - and hence the minimal time ?warning_minimal_duration before the time ?act_time of ?act - to prevent ?act, AND 2) a) ?a has explicitly declared that ?act may be performed on him, or b) i) ?e has included ?act on him in his principles, and ii) the rule of the land (state, company, ...) has not forbidden ?act on ?a, iii) if only one agent must perform ?a, - the competency or willingness of ?e to do ?act must not have been SORPFs-majoritarily-invalidated with respect to ?SORPFs, and - there is no agent ?e2 different from ?e that would be willing to do ?a and such that the proposition "?e2 would be better than ?e to do ?a" is SORPFs-majoritary-approved w.r.t. ?SORPFs, and //thus, role-related powers/responsabilities can be denied for any ?act iv) * no agent ?a among ?as has used ?warning_minimal_duration to send ?e a PP which, with respect to the SORPFs of the ?as, SORPFs-majoritarily-invalidates-or-betters (note: "majoritarily" can be replaced by another voting rule if the ?as majoritarily agree), or * ?e has been able to SORPFs-invalidate-or_better each SORPFs-invalidation-or-betterment that he received and has given enough time to the ?as to SORPFs-invalidates-or-betters any SORPFs-invalidation-or-betterment he sent. The cycle of mutual SORPFs-invalidation-or-betterment evetually/quickly stops/converges (since each step relies/brings on additional precision: => transitive, not arg) but may force ?e to change ?t and ?act). In case ?act is an un-allowed decision, enforcing it is not allowed. /* pas de décision sans fournir aux personnes concernées non seulement l'opportunité de prouver qu'une meilleure solution existe, mais aussi une contre-preuve pour toute pseudo-meilleure-solution fournie. Méthode de choix : //e-mail du 17 mars En cas de divergences sur des choix qui ne relèvent que de préférences, je voterai pour la préférence majoritaire (parmi les préférences exprimées sur la mailing list citée plus haut), à main levée lorsque possible. En cas de divergence sur des choix qui ne relèvent pas que de préférences, je voterai pour l'opinion majoritaire parmi celles dont les contre-arguments n'ont pas été eux-même logiquement contre-argumentés. Eh oui, transparence, cohérence et quelques efforts (sauf pour ceux qui s'abstiennent) sont requis pour diminuer les problèmes associés à toute méthode de vote et, en particulier, les votes "à la majorité". Cependant, si vous choisissez - via ce précédent système de choix - un autre système de choix, j'utiliserai ce dernier. */ R11: salary for a work ?w (requiring a competency ?wc) done by a person ?p (having a competency ?pc for ?w) = f1(evaluation of ?w w.r.t. its specification) + f2(number of hours to acquire ?wc) + f3(number of hours spent to do ?w) + f4(number of hours spent to do ?w - average number of hours that a person with competency ?pc would take to do ?w) ./agentsPublics_protectionFonctionnelle_deontologie.pdf see also in RIFIA 2015 trick that solves many constraints by generalization on fairness+effectiveness criteria: provably minimalyComplete+consistent (and hence not voted not un-votable and auto-applying) democratic/fair meta-meta-laws about decision-making (subtyped by meta-laws/law decision making; laws subtype meta-law decision-making and prescribe decision making except for laws; this permits decision-making not to follow meta-meta-laws if fairly/democratically decided): no decision for others (concerned people) without i) informing them in advance ot the fact, rationale (criteria, ...), decision-voting method (or method criteria and their weights), ... at this time (before the decision), the laws(/status) can change if the laws or the meta-laws allow the laws to be chaged before a decision; if so, they are always "democratic"/representative ii) counter-proof that other proposed solutions are more "globally better (fair, ...) over time", iii) allowing them to correct/change the decision (and its facts, method, ...) for prooved "globally better one over time" (greater good of the greater number). "equals should be treated equally, and unequals unequally, in proportion to the relevant similarities and differences" [Aristotle BC 350]. x + a.(1-x) = x +a - a.x = a + x.(1-a) x.(1-b) Distributive Justice for Self-Organised Common-Pool Resource Management p: 8,9begin,9end ** pre-specified criteria + 3 "fairness" criteria + cf. "limiting the alternative set to two alternatives" + cf. end ** ** ** P S R R P S R Impressive. Hidden rules in the "autonomic Mechanisms/Equations"? -->