• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
          • Logic-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-inductive-proof
          • Introduction-to-rewrite-rules-part-1
          • Introduction-to-key-checkpoints
          • Introduction-to-rewrite-rules-part-2
          • Logic-knowledge-taken-for-granted-propositional-calculus
          • Geneqv
          • Introduction-to-a-few-system-considerations
          • Refinement-failure
          • Introduction-to-the-database
          • Programming-knowledge-taken-for-granted
          • Logic-knowledge-taken-for-granted-rewriting
          • Introductory-challenge-problem-4-answer
          • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
          • Introduction-to-hints
          • Dealing-with-key-combinations-of-function-symbols
          • Architecture-of-the-prover
          • Further-information-on-rewriting
          • Frequently-asked-questions-by-newcomers
          • Specific-kinds-of-formulas-as-rewrite-rules
          • Strong-rewrite-rules
          • Practice-formulating-strong-rules-3
          • Practice-formulating-strong-rules-1
          • Practice-formulating-strong-rules-6
          • Generalizing-key-checkpoints
          • Logic-knowledge-taken-for-granted-q1-answer
          • Example-inductions
          • Logic-knowledge-taken-for-granted-q2-answer
          • Logic-knowledge-taken-for-granted-rewriting-repeatedly
          • Introductory-challenge-problem-4
          • Equivalent-formulas-different-rewrite-rules
          • Post-induction-key-checkpoints
          • Special-cases-for-rewrite-rules
          • Example-induction-scheme-with-accumulators
          • Practice-formulating-strong-rules-5
          • Practice-formulating-strong-rules
          • Practice-formulating-strong-rules-2
          • Introductory-challenges
          • Logic-knowledge-taken-for-granted-equals-for-equals
          • Logic-knowledge-taken-for-granted-evaluation
          • Example-induction-scheme-nat-recursion
          • Example-induction-scheme-down-by-2
          • Logic-knowledge-taken-for-granted-instance
          • Introductory-challenge-problem-3-answer
          • Example-induction-scheme-on-lists
          • Example-induction-scheme-upwards
          • Example-induction-scheme-with-multiple-induction-steps
          • Practice-formulating-strong-rules-4
          • Logic-knowledge-taken-for-granted-q3-answer
          • Example-induction-scheme-binary-trees
          • Introductory-challenge-problem-3
          • Introductory-challenge-problem-1
          • Logic-knowledge-taken-for-granted-base-case
          • Introductory-challenge-problem-1-answer
          • Example-induction-scheme-on-several-variables
          • Introductory-challenge-problem-2-answer
          • Introductory-challenge-problem-2
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Introduction-to-the-theorem-prover

Introductory-challenges

Challenge problems for the new ACL2 user

Do each of the problems. In each case, start with a fresh ACL2 (or undo all effects of previous events with :ubt! 1). This may require that you ``re-discover'' the same lemma more than once in different problems, but recognizing the need for something you used in some previous project is part of the training.

We recommend that you follow The Method and consult the documentation as needed — but that you not look at our answers until you're well and truly baffled!

See introductory-challenge-problem-1 (Answer: introductory-challenge-problem-1-answer)

See introductory-challenge-problem-2 (Answer: introductory-challenge-problem-2-answer)

See introductory-challenge-problem-3 (Answer: introductory-challenge-problem-3-answer)

See introductory-challenge-problem-4 (Answer: introductory-challenge-problem-4-answer)

In addition to these explicit challenge problems designed for beginners, the ACL2 documentation has many example solutions to problems (not always phrased in the question/answer format here). If you are looking for other examples, you should consider

annotated-ACL2-scripts (Answer: the answers are given in the examples)

When you've done the problems and compared your solutions to ours, use your browser's Back Button now to return to introduction-to-the-theorem-prover.