[doc] Do not use utf-8 symbols directly.

doc/acas_xu.rst

@@ -63,37 +63,38 @@ There are several functional properties one may want to verify on this system, f
 * guarantee that the system will never output an advisory that may result in a collision
 * guarantee that the system will not output a Strong advisory where a Weak variant would be enough
 
-Authors of [Katz2017]_ propose ten properties to verify. We
-will reproduce the two first here, and try to check whether a
-given neural network respects it. 
+Authors of [Katz2017]_ propose ten properties to verify. We will reproduce the
+two first here, and try to check whether a given neural network respects it.
 
-**property** 
+**property**
     :math:`\phi_1`
 
 **definition**
-    If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will always be below a certain fixed threshold.
+    If the intruder is distant and is significantly slower than the ownship, the
+    score of a COC advisory will always be below a certain fixed threshold.
 
 **input constraints**
 
-   * :math:`\rho` ≥ 55947.691
-   * :math:`v_{own}` ≥ 1145
-   * :math:`v_{int}` ≤ 60
+   * :math:`\rho` :math:`\geq` 55947.691
+   * :math:`v_{own}` :math:`\geq` 1145
+   * :math:`v_{int}` :math:`\leq` 60
 
 **desired output property**
 
-   * :math:`COC` ≤ 1500
+   * :math:`COC` :math:`\leq` 1500
 
-**property** 
+**property**
     :math:`\phi_2`
 
 **definition**
-    If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will never be maximal.
+    If the intruder is distant and is significantly slower than the ownship, the
+    score of a COC advisory will never be maximal.
 
 **input constraints**
 
-   * :math:`\rho` ≥ 55947.691
-   * :math:`v_{own}` ≥ 1145
-   * :math:`v_{int}` ≤ 60
+   * :math:`\rho` :math:`\geq` 55947.691
+   * :math:`v_{own}` :math:`\geq` 1145
+   * :math:`v_{int}` :math:`\leq` 60
 
 **desired output property**
 
@@ -116,15 +117,13 @@ earlier. We will call our theory `ACAS_XU_P1`.
    theory ACAS_XU_P1
    end
 
-We will need to write down some numerical values. As of now,
-CAISAR support writting values using floating point arithmetic. 
-Why3 defines a float type and the relevant arithmetic
-operations according to the IEEE floating
-point standard in a theory, astutely called ``ieee_float``.
-Specifically, we will import the ``Float64`` subtheory, that
-defines everything we need for 64 bit precision floating
-point numbers.
-We thus import it in our theory using the ``use`` keyword.
+We will need to write down some numerical values. As of now, CAISAR support
+writting values using floating point arithmetic. Why3 defines a float type and
+the relevant arithmetic operations according to the IEEE floating point standard
+in a theory, astutely called ``ieee_float``. Specifically, we will import the
+``Float64`` subtheory, that defines everything we need for 64 bit precision
+floating point numbers. We thus import it in our theory using the ``use``
+keyword.
 
 Our file looks like this so far:
 
@@ -134,13 +133,15 @@ Our file looks like this so far:
      use ieee_float.Float64
    end
 
-We would like to verify our propety given a certain neural network.
-To do this, we can write the filename in our theory.
-Internally, when provided with a neural network file, CAISAR will perform some basic sanity checks (mainly, checks that the network is in a supported format).
-If those checks pass, then CAISAR will internally build a theory, named as the original neural network. This theory will contain two subtheories that provide
-logical symbols we can use in our theory: ``AsTuple`` and ``AsArray``.
-We will only consider the ``AsTuple`` subtheory for this tutorial.
-CAISAR currently supports neural network in ONNX and NNet format.
+We would like to verify our propety given a certain neural network. To do this,
+we can write the filename in our theory. Internally, when provided with a neural
+network file, CAISAR will perform some basic sanity checks (mainly, checks that
+the network is in a supported format). If those checks pass, then CAISAR will
+internally build a theory, named as the original neural network. This theory
+will contain two subtheories that provide logical symbols we can use in our
+theory: ``AsTuple`` and ``AsArray``. We will only consider the ``AsTuple``
+subtheory for this tutorial. CAISAR currently supports neural network in ONNX
+and NNet format.
 
 This theory is equivalent to the following WhyML file:
 

doc/usage.rst

@@ -7,10 +7,10 @@ Property verification
 ---------------------
 
 CAISAR can be used to verify properties on neural networks.
-The prototype command is ``caisar verify --solver=SOLVER property.mlw``
-File property.mlw defines the goal you want to verify,
+The prototype command is ``caisar verify --prover=PROVER property.mlw``.
+File ``property.mlw`` defines the goal you want to verify,
 written in the Whyml language.
-Example of .mlw files can be seen in tests folder.
+Example of ``.mlw`` files can be seen in tests folder.
 
 External verifiers detection
 ----------------------------