Formatting; Jose's changes 2

contrib/systems.md/nelson-oppen/hereditarily-finite-set.md

@@ -2,12 +2,12 @@ Hereditarily Finite Sets with Reals
 -----------------------------------
 
 In this example, we demonstrate the combination algorithm with non-convex theories -- non-linear
-real arithmetic and hereditarily finite sets. Hereditarily finite sets is an example of a theory
-that cannot be implemented in CVC4 or Yices2 because of its use of recursive algebraic data types with
-equations identifying terms. Hereditarily finite sets (HFS) are a model of set theory without
-the axiom of infinity. Although hereditarily finite sets are expressive enough to encode constructs
-like the integers and the natural numbers, its initial model is a countable model and so cannot encode the real
-numbers.
+real arithmetic and hereditarily finite sets. Hereditarily finite sets is an example of a theory not
+currently definable in CVC4 or Yices2 because of its use of algebraic data types modulo axioms like
+associativity-commutativity and having FVP equations. Hereditarily finite sets (HFS) are a model of
+set theory without the axiom of infinity. Although hereditarily finite sets are expressive enough to
+encode constructs like the integers and the natural numbers, its initial model is a countable model
+and so cannot encode the real numbers.
 
 ```test
 set include BOOL off .
@@ -31,8 +31,9 @@ Both `X`s and `Set`s are `Magma`s.
     vars S        : Set   .
 ```
 
-The elements of a hereditarily finite set are constructed inductively from three constructors.
-First, `empty` is a `Set`:
+The elements of a hereditarily finite set can be elements of the parameter sort `X` of "atomic
+elements", or can be other hereditarily constructed inductively from the following three
+constructors. First, `empty` is a `Set`:
 
 ``` {.test .njr-thesis}
     op empty :             -> Set                                       [ctor] .
@@ -169,10 +170,10 @@ reduce var-sat( upModule('HFS-REAL, true)
               ) == true .
 ```
 
-Finally we, check the satisfiability the formula $\{ x^2 , y^2, z^2 \} \subseteq \{ a \} \land x \ne y$. i.e. "is
+Finally, we check the satisfiability of the formula $\{ x^2 , y^2, z^2 \} \subseteq \{ a \} \land x \ne y$. i.e. "is
 it possible for the set of squares of three numbers, two of which must be distinct, to be a
 subset of a set with a single element." This is indeed possible, since every positive real number
-has two distinct square roots. Since set union is idemopotent, if the two distinct numbers are
+has two distinct square roots. Since set union is idempotent, if the two distinct numbers are
 additive inverses of each other and the third is equal to either, then the proposition would indeed
 be satisfied.
 
@@ -225,12 +226,12 @@ Initially, a few equalities are propagated from the theory of hereditarily finit
 'HFS-REAL: => 'z2:Real ?= 'A:Real
 ```
 
-Since no more identifications of variables are implied on their own and the theories are convex, the
-algorithm must check whether a disjunction of identifications is implied by either of the theories,
-and indeed $x = z \lor y = z$ is implied. The algorithm splits the search space on the remaining
-candidate equalities ($a = x$, $a = y$, $a = z$, $x = y$, $z = z$ and $y = z$). It first tries the
-case where $a = x$ and finds that there are satisfiabile arrangements (this can happen when
-$a = x = 1$). It then splits the search space again, but finds that there are no arrangements
+Since no more identifications of variables are implied on their own and the theories are not convex,
+the algorithm must check whether a disjunction of identifications is implied by either of the
+theories, and indeed $x = z \lor y = z$ is implied. The algorithm splits the search space on the
+remaining candidate equalities ($a = x$, $a = y$, $a = z$, $x = y$, $z = z$ and $y = z$). It first
+tries the case where $a = x$ and finds that there are satisfiabile arrangements (this can happen
+when $a = x = 1$). It then splits the search space again, but finds that there are no arrangements
 $a = y$ possible (since that implies that $x = y$). However the case where $a = z$ is satisfiable.
 This causes the the equality $x = z$ to be propagated. Now, since no further equalities or
 disjunctions thereof hold, the algorithm concludes that the formula is satisfiable.

contrib/systems.md/nelson-oppen/matrix.md

@@ -45,7 +45,7 @@ endfm
 
 Next, we define matrix multiplication, determinant and identity as \emph{definitional extensions} of
 the theory of matrices. That is, these new functions are fully defined in terms of the theory of
-matrices itself and can always be "evaluated away." This important to meet the Nelson-Oppen
+matrices itself and can always be "evaluated away." This is important to meet the Nelson-Oppen
 theory disjointness requirement, as explained below.
 
 \begin{verbatim}
@@ -171,10 +171,9 @@ endfm
 set print attribute on .
 ```
 
-We cannot, at the moment, use this specification as is, because the Nelson-Oppen
-implementation does not support view yet. We execute the the following query
-against an equivalent specification of real matrices:
-
+We cannot, at the moment, use this specification as is, because the Nelson-Oppen implementation does
+not support views yet. Instead, we execute the the following query against an equivalent
+specification of real matrices:
 
 ``` {.test .njr-thesis}
 reduce in MATRIX-TEST : nelson-oppen-valid(
@@ -196,7 +195,7 @@ in the theory of reals:
  /\ 'p12:Real ?= '_+_['_*_['a11:Real, 'b12:Real],'_*_[ 'a12:Real, 'b22:Real]] 
  /\ 'p21:Real ?= '_+_['_*_['a21:Real, 'b11:Real],'_*_[ 'a22:Real, 'b21:Real]] 
  /\ 'p22:Real ?= '_+_['_*_['a21:Real, 'b12:Real],'_*_[ 'a22:Real, 'b22:Real]] 
- /\ '0/1.Real ?= '_-_['_*_[ 'a11:Real, 'a22:Real],'_*_[ 'a12:Real, 'a21:Real]]
+ /\ '0/1.Real ?= '_-_['_*_['a11:Real, 'a22:Real],'_*_[ 'a12:Real, 'a21:Real]]
 ```
 
 and, in the theory of Matrices:
@@ -228,8 +227,8 @@ unsatisfiable and the original formula must be valid.
 
 It turns out that if we combine this module with the Integers instead of the Reals, we can prove
 something stronger: that any invertible matrix must have determinant $\pm 1$. Unfortunately, CVC4 is
-not able to solve the non-linear arithmetic needed to prove this. We must instead turn to the Yices2
-solver, the other SMT solver available in Maude. Even so, the default configuration for Yices2 does
+not able to solve the non-linear arithmetic needed to prove this. We must instead turn to the Yices
+solver, the other SMT solver available in Maude. Even so, the default configuration for Yices does
 not enable the solver for non-linear arithmetic (MCSAT), and running this example involved modifying
 the Maude C++ source code to enable that configuration. Even so, the computational difficulty
 involved in solving non-linear integer arithmetic forced us to restrict the proof to
@@ -305,5 +304,6 @@ Similar equalities are propagated:
 'MATRIX-INTEGER: => 'p11:Integer ?= 'p22:Integer
 ```
 
-leading to the same contradiction: that $0 = 1$, allowing us to conclude that
-the original formula is in fact valid.
+leading to a complex contradiction forcing some elements to be inverses of others in an impossible
+way, allowing us to conclude that the original formula is valid.
+

contrib/tools/meta.md/nelson-oppen-combination.md

@@ -229,7 +229,7 @@ The `nelson-oppen-valid` function converts a validity check into a satisfiabilit
 
 Given a quantifier free formula `PHI` in the set of theories `TFS` (each tagged with information
 regarding covexitivity, and information about which procedure to use for checking sat), we first
-convert it to the disjunctive normal form (DNF) and simplify it (e.g. $\bot \land \phi$ becomes
+convert it to disjunctive normal form (DNF) and simplify it (e.g. $\bot \land \phi$ becomes
 $\bot$).
 
 ```{ .maude .njr-thesis }
@@ -245,7 +245,7 @@ The algorithm then considers each disjunction separately.
      .
 ```
 
-We then purify each disjunction into a disjunction of "pure" atoms each wellformed in the signature
+We then purify each mixed disjunct into a conjunction of "pure" atoms each wellformed in the signature
 of one of the theories, and tagged with the appropriate information.
 
 ```{ .maude .njr-thesis }
@@ -299,7 +299,10 @@ where $\SharedVariables_{s_i}$ is the subset of shared variables in the connecte
 ```
 
 Next, we apply the equality propagation inference rule. If any identification of variables is
-implied by a theory, we propagate that identification to the other theories.
+implied by a theory, we propagate that identification to the other theories by replacing all
+occurrences of the variable in the left hand side with that on the right hand side in all formulae
+and the candidate equalities. Performing the substitution instead of merely adding the equality to
+the formula has the advantage of reducing the number of candidate equalities we need to try.
 
 ```{ .maude .njr-thesis }
    ceq $nosat.ep(( tagged(PHI1, ('mod > ME1); TS1)
@@ -325,8 +328,8 @@ If there are no variables left to identify, then the formula is satisfiable
     eq $nosat.split(TFS, mtForm) = true .
 ```
 
-However, if there some disjunction of identifications implied and we are in a non-convex theory, we
-"split". i.e. we try each of the possible identification left in turn and see if atleast one of them
+However, if some disjunction of identifications is implied and we are in a non-convex theory, we
+"split". i.e. we try each of the possible identification left in turn and see if at least one of them
 is satisfiable.
 
 ```{ .maude .njr-thesis }
@@ -369,5 +372,9 @@ We use `$nosat.split.genEqs` to generate this disequality of sat problems.
                        , mtForm, DISJ?2)
      = false
      .
+```
+
+``` {.maude}
 endfm
 ```
+