An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

DOI10.1007/BF00244993zbMATH Open0614.68062OpenAlexW2008655451MaRDI QIDQ1819945FDOQ1819945

Authors: David M. Russinoff 

Publication date: 1985

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00244993

Recommendations

• A mechanical proof of quadratic reciprocity
• scientific article; zbMATH DE number 4033137
• Fermat, Euler, Wilson -- three case studies in number theory
• scientific article; zbMATH DE number 3880145
• Proof movie -- a proof with the Boyer-Moore prover

zbMATH Keywords

number theoryautomatic theorem provingBoyer-Moore theorem proverWilson's theorem

Mathematics Subject Classification ID

Cited In (8)

• Title not available (Why is that?)
• Title not available (Why is that?)
• A theorem prover for a computational logic
• A mechanical proof of quadratic reciprocity
• Verification of the Miller-Rabin probabilistic primality test.
• Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
• Title not available (Why is that?)
• Fermat, Euler, Wilson -- three case studies in number theory

Uses Software

• NQTHM

This page was built for publication: An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1819945)