Automated Theorem-Proving Research In The Fifth Generation Computer Systems Project: Model Generation Theorem Provers

Citation

Stickel, M. E. (1993). Automated theorem-proving research in the Fifth Generation Computer Systems Project: Model generation theorem provers. Future Generation Computer Systems, 9(2), 143-152.

Abstract

One of the successful outcomes of the Fifth Generation Computer Systems Project is the development of Model Generation Theorem Provers (MGTPs). MGTPs have solved previously open problems in finite algebra, produced rapid proofs of condensed detachment problems, and are providing an inferential infrastructure for knowledge-processing research at ICOT. They successfully exploit the Fifth Generation Projects KL1 logic programming language and parallel inference machines to achieve high performance and parallel speedup. This paper describes some of the key properties of MGTPs, reasons for their successes, and possible areas for future improvement.

↓ Download

Read more from SRI

  • An arid, rural Nevada landscape

    Can AI help us find valuable minerals?

    SRI’s machine learning-based geospatial analytics platform, already adopted by the USGS, is poised to make waves in the mining industry.

  • Two students in a computer lab

    Building a lab-to-market pipeline for education

    The SRI-led LEARN Network demonstrates how we can get the best evidence-based educational programs to classrooms and students.

  • Code reflected in a man's eyeglasses

    LLM risks from A to Z

    A new paper from SRI and Brazil’s Instituto Eldorado delivers a comprehensive update on the security risks to large language models.