• Top
    • Documentation
      • Xdoc
      • ACL2-doc
      • Recursion-and-induction
      • Loop$-primer
      • 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::sawada00
          • Bib::mccarthy62
          • Bib::bm79
          • 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
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Operational-semantics-3__annotated-bibliography

    Bib::moore73

    J S. Moore, “Computational Logic: Structure Sharing and Proof of Program Properties, University of Edinburgh, Ph.D. dissertation, 1973.



    Relevance: details of the Edinburgh Pure Lisp Theorem Prover (PLTP)



    ———

    Part II of Moore's dissertation describes the Edinburgh Pure Lisp Theorem Prover (PLTP) in detail. The work was carried out jointly with Bob Boyer.