| … | … | @@ -101,10 +101,10 @@ think of this process as being a kind of generation, where rules and |
| 101 | 101 | axioms are specific building blocks that are assembled. |
| 102 | 102 | |
| 103 | 103 | The rules and axioms are jigsaw pieces; theorem proving is the assembly |
| 104 | | of these. If it is free an unconstrained, then it is generation; if its |
| 104 | of these. If it is free and unconstrained, then it is generation; if its |
| 105 | 105 | constrained, then some sort of satisfiability solver is needed: the |
| 106 | | jigsaw much assemble so as to build be bridge between constraints. The |
| 107 | | satisfiability algorithm must be fast, but also the bridge that is build |
| 106 | jigsaw must assemble so as to build a bridge between constraints. The |
| 107 | satisfiability algorithm must be fast, but also the bridge that is built |
| 108 | 108 | must be minimal or optimal in some way. |
| 109 | 109 | |
| 110 | 110 | ### Minimization |