Admin/website/logics.html
changeset 16272 bcf05183df9e
parent 16240 95cc0e8f8a17
child 16575 15d5f8e729fe
equal deleted inserted replaced
16271:5aba3dc670e8 16272:bcf05183df9e
    90       based on primitive inferences (by employing the built-in mechanisms of
    90       based on primitive inferences (by employing the built-in mechanisms of
    91       <em>Isabelle/Pure</em>, in particular higher-order unification and resolution). For
    91       <em>Isabelle/Pure</em>, in particular higher-order unification and resolution). For
    92       sizable applications some degree of automated reasoning is essential.
    92       sizable applications some degree of automated reasoning is essential.
    93       Instantiating existing tools like the classical tableau prover involves only
    93       Instantiating existing tools like the classical tableau prover involves only
    94       minimal ML-based setup. One may also write arbitrary proof procedures or even
    94       minimal ML-based setup. One may also write arbitrary proof procedures or even
    95       theory extension packages in ML, without breaching system soundness (Isabelle
    95       theory extension packages in ML, without breaking system soundness (Isabelle
    96       follows the well-known <em>LCF system approach</em> to achieve a secure
    96       follows the well-known <em>LCF system approach</em> to achieve a secure
    97       system).</p>
    97       system).</p>
    98     </div>
    98     </div>
    99     <div class="hr"><hr/></div>
    99     <div class="hr"><hr/></div>
   100     <?include file="//include/footer.include.html"?>
   100     <?include file="//include/footer.include.html"?>