Update Wed Mar 27 11:37:26 AM EDT 2024

implementing_first_order_logic.html

@@ -425,6 +425,8 @@ <h2><span class="section-number">11.3. </span>Formulas<a class="headerlink" href
 
 <span class="k">#eval</span> <span class="n">myWorld.show</span>
 
+<span class="bp">#</span><span class="mi">3</span><span class="n">d_world</span> <span class="n">myWorld</span>
+
 <span class="c">/-</span>
 <span class="cm">-----------------------------------------</span>
 <span class="cm">| D- |    |    |    | D+ |    |    |    |</span>
@@ -643,7 +645,7 @@ <h2><span class="section-number">11.3. </span>Formulas<a class="headerlink" href
 it computes the association list and uses <cite>usolve</cite> to turn it into a
 substitution.</p>
 <div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="n">partial</span> <span class="kd">def</span> <span class="n">usolve</span> <span class="o">(</span><span class="n">env</span> <span class="o">:</span> <span class="n">AssocList</span> <span class="n">String</span> <span class="n">FOTerm</span><span class="o">)</span> <span class="o">:</span> <span class="n">AssocList</span> <span class="n">String</span> <span class="n">FOTerm</span> <span class="o">:=</span> <span class="n">Id.run</span> <span class="k">do</span>
-  <span class="k">let</span> <span class="n">env&#39;</span> <span class="o">:=</span> <span class="n">env.mapVal</span> <span class="o">(</span><span class="n">subst</span> <span class="n">env</span><span class="o">)</span>
+  <span class="k">let</span> <span class="n">env&#39;</span> <span class="o">:=</span> <span class="n">env.mapVal</span> <span class="o">(</span><span class="k">fun</span> <span class="n">_</span> <span class="bp">=&gt;</span> <span class="n">subst</span> <span class="n">env</span><span class="o">)</span>
   <span class="k">if</span> <span class="n">env&#39;</span> <span class="bp">==</span> <span class="n">env</span> <span class="k">then</span> <span class="n">env</span> <span class="k">else</span> <span class="n">usolve</span> <span class="n">env&#39;</span>
 
 <span class="n">partial</span> <span class="kd">def</span> <span class="n">fullUnify</span> <span class="o">(</span><span class="n">eqs</span> <span class="o">:</span> <span class="n">List</span> <span class="o">(</span><span class="n">FOTerm</span> <span class="bp">×</span> <span class="n">FOTerm</span><span class="o">))</span> <span class="o">:</span> <span class="n">Option</span> <span class="o">(</span><span class="n">AssocList</span> <span class="n">String</span> <span class="n">FOTerm</span><span class="o">)</span> <span class="o">:=</span>

index.html

@@ -181,9 +181,13 @@ <h1>Logic and Mechanized Reasoning<a class="headerlink" href="#logic-and-mechani
 </ul>
 </li>
 <li class="toctree-l1"><a class="reference internal" href="decision_procedures_for_first_order_logic.html">12. Decision Procedures for First-Order Logic</a><ul>
-<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#linear-arithmetic">12.1. Linear arithmetic</a></li>
-<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#linear-integer-arithmetic">12.2. Linear integer arithmetic</a></li>
-<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#equality">12.3. Equality</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#equality">12.1. Equality</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#implementing-congruence-closure">12.2. Implementing congruence closure</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#deciding-universal-sentences">12.3. Deciding universal sentences</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#linear-arithmetic">12.4. Linear arithmetic</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#implementing-fourier-motzkin">12.5. Implementing Fourier-Motzkin</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#a-full-decision-procedure">12.6. A full decision procedure</a></li>
+<li class="toctree-l2"><a class="reference internal" href="decision_procedures_for_first_order_logic.html#other-theories">12.7. Other theories</a></li>
 </ul>
 </li>
 <li class="toctree-l1"><a class="reference internal" href="using_smt_solvers.html">13. Using SMT solvers</a><ul>

proof_systems_for_first_order_logic.html

@@ -110,7 +110,7 @@
 though we do not provide detailed proofs here.</p>
 <section id="axiomatic-systems">
 <h2><span class="section-number">14.1. </span>Axiomatic systems<a class="headerlink" href="#axiomatic-systems" title="Link to this heading"></a></h2>
-<p>We have already discussed equational reasoning in <a class="reference internal" href="decision_procedures_for_first_order_logic.html#section-equality"><span class="std std-numref">Section 12.3</span></a>.
+<p>We have already discussed equational reasoning in <a class="reference internal" href="decision_procedures_for_first_order_logic.html#section-equality"><span class="std std-numref">Section 12.1</span></a>.
 We have seen that the natural rules for equality are given by reflexivity, symmetry,
 transitivity, and congruence with respect to functions and relations.
 These can be expressed as rules, but also as first-order axioms:</p>
@@ -425,7 +425,7 @@ <h2><span class="section-number">14.4. </span>Natural deduction<a class="headerl
 \]</div></div></blockquote>
 <p>In the right rule for <span class="math notranslate nohighlight">\(\forall\)</span> and the left rule for <span class="math notranslate nohighlight">\(\exists\)</span>, the eigenvariable
 condition amounts to the requirement that <span class="math notranslate nohighlight">\(x\)</span> is not free in any formula other than
-<span class="math notranslate nohighlight">\(A\)</span>. The rules for equality are the same as in <a class="reference internal" href="decision_procedures_for_first_order_logic.html#section-equality"><span class="std std-numref">Section 12.3</span></a>,
+<span class="math notranslate nohighlight">\(A\)</span>. The rules for equality are the same as in <a class="reference internal" href="decision_procedures_for_first_order_logic.html#section-equality"><span class="std std-numref">Section 12.1</span></a>,
 except that in all the rules, we allow a set <span class="math notranslate nohighlight">\(\Gamma\)</span> of formulas on the left side
 of the sequent.</p>
 </section>