
<html>

  <head>

    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">

  </head>

  <body>

    <div class="moz-cite-prefix">Hello,</div>

    <div class="moz-cite-prefix"><br>

    </div>

    <div class="moz-cite-prefix">Le 03/01/2021 à 08:59, Peter Bernard

      Ladkin a écrit :<br>

    </div>

    <blockquote type="cite"

      cite="mid:0033861b-7fed-b458-8e4f-cab068fe67e7@causalis.com">

      <blockquote type="cite" style="color: #007cff;">So a proof-checker

        is a much

        <br>

        simpler program than a proof-creator: </blockquote>

      Not necessarily. Decision procedures can work in arbitrarily

      complicated ways. Many if not most proof checkers nowadays employ

      decision procedures for subtheories, I understand (for example,

      varieties of Pressburger arithmetic).</blockquote>

    <p>There are two commonly used definitions for a "proof-checker":</p>

    <ol>

      <li>The simplest program to check a proof using only the axioms of

        the logic. For example, "coqchk" tool in Coq proof assistant:

<a class="moz-txt-link-freetext" href="https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html#compiled-libraries-checker-coqchk">https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html#compiled-libraries-checker-coqchk</a>

        . This is Begnara's meaning<br>

      </li>

      <li>An automated prover which, as Ladkin said can used arbitrarily

        complicated decision procedures and thus is far form being free

        of bugs. Note that in some cases it is possible for a proof

        assistant to reconstruct the proof made by an automated prover

        and thus gain the confidence of case 1. Isabelle proof assistant

        is notoriously known for this with its Sledgehammer

        infrastructure.</li>

    </ol>

    <p>Best regards,<br>

      D. Mentré</p>

    <p><br>

    </p>

  </body>

</html>