[SystemSafety] Faults in maths proofs

[David MENTRÉ]

Hello,

Le 03/01/2021 à 08:59, Peter Bernard Ladkin a écrit :
>> So a proof-checker is a much
>> simpler program than a proof-creator: 
> 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).

There are two commonly used definitions for a "proof-checker":

 1. The simplest program to check a proof using only the axioms of the
    logic. For example, "coqchk" tool in Coq proof assistant:
    https://coq.inria.fr/distrib/current/refman/practical-tools/coq-commands.html#compiled-libraries-checker-coqchk
    . This is Begnara's meaning
 2. 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.

Best regards,
D. Mentré


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20210103/6345ff04/attachment.html>