An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
type: Item
instance of: scholarly article
title: An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
zbMATH Open document ID: 0614.68062
DOI: 10.1007/BF00244993
author: David M. Russinoff
published in: Journal of Automated Reasoning
publication date: 1985-01-01T00:00:00Z
review text: This paper describes the use of the Boyer-Moore theorem prover in mechanically generating a proof of Wilson's theorem: for any prime p, (p- 1)! and p-1 are congruent modulo p. The input to the theorem prover consists of a sequence of three function definitions and forty-two propositions to be proved. The proofs generated by the system are based on a library of lemmas relating to list manipulation and number theory, including Fermat's theorem.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3995080
zbMATH Keywords: automatic theorem proving
zbMATH Keywords: Boyer-Moore theorem prover
zbMATH Keywords: number theory
zbMATH Keywords: Wilson's theorem
describes a project that uses: NQTHM
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00244993
OpenAlex ID: W2008655451
description: scientific article; zbMATH DE number 3995080