documentation

README.org

@@ -45,6 +45,9 @@
   4. Computes the Belief value associated to each member of
      $\mathcal{W}_\subseteq(B, \mu)$.
 
+
+  We plan to add the computation of the CSRG and CSRW revision operators.
+  
 [fn:1] Raïda Ktari, Mohamed Ayman Boujelben,Éric Würbel, "Toward
 credible belief base revision", Int. J. Approx. Reason., Vol. 162,
 art. 109007, 2023.
@@ -90,15 +93,186 @@ art. 109007, 2023.
 
   You can use =~= in the clingo path.
   
-* Command line syntax
+* Command line
 
   The syntax is printed on ~stderr~ when un run ~wbel~ without argument.
 
+  There are two main usages, as described in the help:
+  - ~wbel [options] kbase_file, mu_file~
+  - ~wbel -r [options] set_description_file~
+
+
+  The first mode is the /normal/ mode, and the second one is the /raw/
+  mode.
+
+  In normal mode, there are two mandatory positional arguments. The
+  first argument, ~kbase_file~, is a path to a file containing the
+  formulae of the belief base. The second argument ~mu_file~ is a path
+  to a file containing the formula by which the belief base must be
+  revised.
+
+  In raw mode, there is only one mandatory positional argument,
+  ~set_description_file~, which is a path to a file containing the
+  description of the structure of a knowledge base and the subsets
+  maximally consistent with the formula by which the base should be
+  revised.
+
+  Some options are incompatible with the raw mode, namely ~--asp~,
+  ~--inclusion-max~, ~--prog~.
+  
+* Running in normal mode
+
+  As stated above, in normal mode, there are two mandatory positional
+  arguments.  The first argument, ~kbase_file~, is a path to a file
+  containing the formulae of the belief base (the belief base will be
+  denoted by $B$).  The second argument ~mu_file~ is a path to a file
+  containing the formula by which the belief base must be revised.
+  This formula will be denoted $\mu$.
+
+  The program computes the belief associated with each subbase
+  maximally consistent (wrt set inclusion) with the formula by which
+  the revision should be performed.
+
+  In this mode, the program starts by the computation of the
+  collection of the subsets of the knowledge base maximally consistent
+  (wrt set inclusion) with the formula by which the revision should be
+  performed. In what follows, we denote this collection by
+  $\mathcal{W}_\subseteq(B,\mu)$. This computation is performed thanks
+  to an ASP program. It is possible to:
+  - print the output of the ASP solver with the ~--asp~ option.
+  - print the content of $\mathcal{W}_\subseteq(B,\mu)$ with the
+    option ~--inclusion-max~.
+  - print the generated ASP program with the ~--prog~ option.
   
-* Running in ~normal~ mode
 ** Syntax of propositional formulae
+
+   Formulae are prolog terms.
+   
+   #+BEGIN_EXAMPLE
+   <formulae> ::= <formula> "." <formulae> | <formula> "."
+   <formula> ::= <formula> <bin-connector> <formula> | "-" <formula> | "(" <formula> ")" | <propositional_atom>
+   <bin-connector> ::= "|" | "&" | "<->" | "->"
+   #+END_EXAMPLE
+   A propositional atom is any prolog ground term, provided that the
+   functor respects the ~[a-z][a-zA-Z_0-9]~.
+   
+   
 ** Example
-* Running in ~raw~ mode
+
+   The example is the one used in [fn:2].
+   The set  $B$ of formulae is discribed in a file ~B.pl~:
+   #+BEGIN_SRC prolog
+     -a & b & c | (-c & (a <-> b)).
+     -a.
+     -a & c | a & b & -c.
+     -a & b | a & -b & -c.
+     c & (-a <-> b).
+     (c & (-a <-> b)) | (a & -b & -c).
+     (a & (-b <->c)) | (-a & b & c).     
+   #+END_SRC
+
+   And the formula $\mu$ is described in a file ~mu.pl~ :
+   #+BEGIN_SRC prolog
+     (-a & -b) | (a & c) | -a & b & -c.
+   #+END_SRC
+
+   If we run  ~wbel~ with these two files as input we obtain:
+   #+BEGIN_SRC shell-session
+   $ wbel B.pl mu.pl
+   Bel(1={[(c&(-a<->b)),(c&(-a<->b)|a& -b& -c),(a&(-b<->c)|-a&b&c)]})=375r1747
+   Bel(2={[(-a&b&c|-c&(a<->b)),-a]})=392r1747
+   Bel(3={[-a,(-a&b|a& -b& -c)]})=392r1747
+   Bel(4={[-a,(-a&c|a&b& -c)]})=392r1747
+   #+END_SRC
+
+   The belef values are rationals, e.g. ~375r1747~ means $375/1747$.
+
+   You can sort the results on belief values:
+   #+BEGIN_SRC shell-session
+   $ wbel --sort B.pl mu.pl
+   Bel(2={[(-a&b&c|-c&(a<->b)),-a]})=392r1747
+   Bel(3={[-a,(-a&b|a& -b& -c)]})=392r1747
+   Bel(4={[-a,(-a&c|a&b& -c)]})=392r1747
+   Bel(1={[(c&(-a<->b)),(c&(-a<->b)|a& -b& -c),(a&(-b<->c)|-a&b&c)]})=375r1747
+   #+END_SRC
+
+   You can avoid the normalization factor in the Dempster combination
+   rule, which does not change the order between subsets. The
+   combination rule is then the conjunctive rule of the Transferable
+   Belief Model:
+   #+BEGIN_SRC shell-session
+   $ wbel --sort --no-norm B.pl mu.pl
+   Bel(2={[(-a&b&c|-c&(a<->b)),-a]})=8r49
+   Bel(3={[-a,(-a&b|a& -b& -c)]})=8r49
+   Bel(4={[-a,(-a&c|a&b& -c)]})=8r49
+   Bel(1={[(c&(-a<->b)),(c&(-a<->b)|a& -b& -c),(a&(-b<->c)|-a&b&c)]})=375r2401
+   #+END_SRC
+  
+
+[fn:2] Raïda Ktari, Mohamed Ayman Boujelben,Éric Würbel, "Toward
+credible belief base revision", Int. J. Approx. Reason., Vol. 162,
+art. 109007, 2023. 
+   
+** prioritized credibility
+
+   This is an exploratory extension, implemented with the
+   ~--prioritized~ option. It considers the belief base as being
+   stratified. In this context, each stratum of the belief base is
+   preceded by a ~stratum__~ fact.
+
+   Stratas are described from the highest priority stratum to the
+   lowest priority stratum.
+
+   For example:
+   #+BEGIN_SRC prolog
+     stratum__.
+     -a & b & c | (-c & (a <-> b)).
+     -a & b | a & -b & -c.
+     stratum__.
+     -a.
+     stratum__.
+     -a & c | a & b & -c.
+     c & (-a <-> b).
+     (c & (-a <-> b)) | (a & -b & -c).
+     (a & (-b <->c)) | (-a & b & c).
+   #+END_SRC
+
+   This describes a stratified belief base $B$ containing three strata, where:
+   - the highest priority stratum $S_1$contains two formulae;
+   - the medium priority stratum $S_2$ contains one formula;
+   - the lowest priority stratum $S_3$ contains four formulae.
+
+
+   Initial basic belief assignment for each set
+   $B_i\in\mathcal{W}_\subseteq(B,\mu)$ is defined as:
+   - $m_{i,\mu}(B_i\cap S_1)=|B_i\cap S_1|/|B|$,
+   - $m_{i,\mu}(B_i\cap S_2)=|B_i\cap S_2|/|B|$,
+   - $m_{i,\mu}(B_i\cap S_3)=|B_i\cap S_3|/|B|$,
+   - $m_{i,\mu}(B)=1-\sum_{j\in\{1,\ldots,3\}}m_{i,\mu}(B_i\cap S_j)$.
+
+
+   Then the initial BBAs are combined using Dempster rule of
+   combination (or the conjunctive rule of the TBM if ~--no-norm~
+   option is specified). Then the belief of $B_i\cap S_j$ is computed
+   for each subbase $B_i$ and each stratum $S_j$. The belief
+   associated to each subbase $B_i$ is then defined as a tuple
+   $(b_1,\ldots,b_m)$, $m$ being the number of strata, the values
+   being sorted by decreasing priority of the strata. This allows the
+   use of lexicographic comparisons to find the base with the highest
+   belief value.
+
+   If we consider the previous base $B$ with the stratification
+   described above, this leads to:
+   #+BEGIN_SRC shell-session
+   $ wbel --sort --no-norm --prioritized B.pl mu.pl
+   Bel(2={[(-a&b|a& -b& -c),-a]})=[100r2401,144r2401,0]
+   Bel(4={[(-a&b&c|-c&(a<->b)),-a]})=[100r2401,144r2401,0]
+   Bel(3={[-a,(-a&c|a&b& -c)]})=[0,144r2401,100r2401]
+   Bel(1={[(c&(-a<->b)),(a&(-b<->c)|-a&b&c),(c&(-a<->b)|a& -b& -c)]})=[0,0,375r2401]
+   #+END_SRC
+   
+* Running in raw mode
 ** Describing belief base and subbases
 ** Example
+** prioritized credibility