[SystemSafety] Faults in maths proofs

[Peter Bernard Ladkin]

On 2021-01-02 22:12 , Roberto Bagnara wrote:
> 
> Nonetheless, properly-said proofs created by programs can be presented
> as sequences of logical statements, each of which either is an axiom
> or can be obtained by means of an inference rule from statements
> occurring earlier in the sequence.  

Not all proof checkers work with Hilbert-Bernays style axiomatics. The three I have worked with 
don't -- the Shostack prover, TLA, and Knuth-Bendix rewrites.

> 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).

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
ClaireTheWhiteRabbit RIP
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20210103/dfb17ea1/attachment.sig>