Verifying Sierpiński and Riesel Numbers in ACL2

Details Verifying Sierpiński and Riesel Numbers in ACL2 Verifying Sierpiński and Riesel Numbers in ACL2

2011-10-21

arxiv.org/abs/1110.4671v1

EPTCS 70, 2011, pp. 20-27

Computer Science

Discrete Mathematics

In Proceedings ACL2 2011, arXiv:1110.4473

Scientific paper

10.4204/EPTCS.70.2

A Sierpinski number is an odd positive integer, k, such that no positive integer of the form k * 2^n + 1 is prime. Similar to a Sierpinski number, a Riesel number is an odd positive integer, k, such that no positive integer of the form k * 2^n + 1 is prime. A cover for such a k is a finite list of positive integers such that each integer j of the appropriate form has a factor, d, in the cover, with 1 < d < j. Given a k and its cover, ACL2 is used to systematically verify that each integer of the given form has a non-trivial factor in the cover.

Affiliated with

Also associated with

No associations

Rating

Verifying Sierpiński and Riesel Numbers in ACL2 does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Verifying Sierpiński and Riesel Numbers in ACL2, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying Sierpiński and Riesel Numbers in ACL2 will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-84674