• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
        • Operational-semantics-3__annotated-bibliography
          • Bib::bhmy89
          • Bib::liu06
          • Bib::bm96
          • Bib::plotkin04b
          • Bib::bgm90
          • Bib::hkms17
          • Bib::bkm96
          • Bib::moore15
          • Bib::bh99
          • Bib::wilding93
          • Bib::plotkin04a
          • Bib::moore03b
          • Bib::mp02
          • Bib::moore19
          • Bib::manolios00
          • Bib::flatau92
          • Bib::hb92
          • Bib::bm05
          • Bib::goel16
          • Bib::bm73
          • Bib::ghk17
          • Bib::wilding92
          • Bib::moore17
          • Bib::moore96
          • Bib::ghkg14
          • Bib::yu92
          • Bib::hunt85
          • Bib::boh03
          • Bib::mmrv06
          • Bib::bm80
          • Bib::bh97
          • Bib::moore99b
          • Bib::moore14
          • Bib::rm04
          • Bib::by96
          • Bib::mccarthy62
          • Bib::bm79
          • Bib::sawada00
          • Bib::moore99a
          • Bib::sh98
          • Bib::rhmm07
          • Bib::kmm00a
          • Bib::ghk13
          • Bib::moore03a
          • Bib::hk12
          • Bib::mp67
          • Bib::young88
          • Bib::bm97
          • Bib::moore73
          • Bib::kmm00b
            • Bib::bevier87
          • Operational-semantics-1__simple-example
          • Operational-semantics-2__other-examples
          • Operational-semantics-5__history-etc
          • Operational-semantics-4__how-to-find-things
        • Real
        • Start-here
          • Gentle-introduction-to-ACL2-programming
          • ACL2-tutorial
          • About-ACL2
            • Recursion-and-induction
            • Operational-semantics
              • Operational-semantics-3__annotated-bibliography
                • Bib::bhmy89
                • Bib::liu06
                • Bib::bm96
                • Bib::plotkin04b
                • Bib::bgm90
                • Bib::hkms17
                • Bib::bkm96
                • Bib::moore15
                • Bib::bh99
                • Bib::wilding93
                • Bib::plotkin04a
                • Bib::moore03b
                • Bib::mp02
                • Bib::moore19
                • Bib::manolios00
                • Bib::flatau92
                • Bib::hb92
                • Bib::bm05
                • Bib::goel16
                • Bib::bm73
                • Bib::ghk17
                • Bib::wilding92
                • Bib::moore17
                • Bib::moore96
                • Bib::ghkg14
                • Bib::yu92
                • Bib::hunt85
                • Bib::boh03
                • Bib::mmrv06
                • Bib::bm80
                • Bib::bh97
                • Bib::moore99b
                • Bib::moore14
                • Bib::rm04
                • Bib::by96
                • Bib::mccarthy62
                • Bib::bm79
                • Bib::sawada00
                • Bib::moore99a
                • Bib::sh98
                • Bib::rhmm07
                • Bib::kmm00a
                • Bib::ghk13
                • Bib::moore03a
                • Bib::hk12
                • Bib::mp67
                • Bib::young88
                • Bib::bm97
                • Bib::moore73
                • Bib::kmm00b
                  • Bib::bevier87
                • Operational-semantics-1__simple-example
                • Operational-semantics-2__other-examples
                • Operational-semantics-5__history-etc
                • Operational-semantics-4__how-to-find-things
              • Soundness
              • Release-notes
              • Workshops
              • ACL2-tutorial
              • Version
              • How-to-contribute
              • Acknowledgments
              • Using-ACL2
              • Releases
              • Pre-built-binary-distributions
              • Common-lisp
              • Installation
              • Mailing-lists
              • Git-quick-start
              • Copyright
              • ACL2-help
          • Miscellaneous
          • Output-controls
          • Bdd
          • Macros
          • Installation
          • Mailing-lists
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Operational-semantics-3__annotated-bibliography

      Bib::kmm00b

      M. Kaufmann, P. Manolios, J S. Moore, Computer-Aided Reasoning: ACL2 Case Studies, Kluwer Academic Publishers, 2000.



      Relevance: tutorial examples of ACL2 applications



      ———

      This book is a companion to bib::kmm00a. It contains fourteen articles by ACL2 experts, explaining how they formalized and solved fourteen different problems. It also includes exercises.