Intelligent CAI course in the first-order logic

AI Applications In CAL
Part of the Lecture Notes in Computer Science book series (LNCS, volume 438)


Our theorem proving system named TTP (which is short for Teaching Theorem Proving) can construct the natural deduction proofs of the first-order logic formulas with quantifiers. It is written in CLISP. It has 4 learning models. Students can use the system to do their logic homework step by step and learn the skills of proving logic theorems. If they don't know how to prove the theorems, they can ask for hints. In our university about 300 students used the system to learn logic and do homework during 3 years, they did 2000 problems in logic.


first-order logic natural deduction resolution tautology theorem proving 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Andrews, P. B., An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Orlando, Academic Pr., Inc., 1986.Google Scholar
  2. [2]
    Bledsoe, W. W., Non-resolution Theorem Proving, Artificial Intelligence 9, 1–35, 1977.CrossRefGoogle Scholar
  3. [3]
    Dafa, Li, Extended Tautology, Journal of Tsinghua University, Vol. 27, No.3, 1987.Google Scholar
  4. [4]
    Manna, Z., Mathematical Theory of Computation, New York, 1974.Google Scholar
  5. [5]
    Pelletier, F. J., Seventy-Five problems for Testing Automatic Theorem provers, J. of Automated Reasoning, Vol. 2, No. 2, 191–216, 1986.Google Scholar
  6. [6]
    Smullyan, R. M., First-Order Logic, Springer-Verlag, New York, 1968.Google Scholar
  7. [7]
    Stanat, D. F. and McAlliister, D. F., Discrete Mathematics in Computer Science, Prentice-Hall, Inc., Englewood Cliffs, N.J., 1977.Google Scholar
  8. [8]
    Suppes Patrick, University-Level Computer-Asisted Instrution At Stanford: 1968–1980.Google Scholar
  9. [9]
    Tremblay, J. P. and Manohar, R., Discrete Mathematial Structures with Applications to Computer Science, New York, McGray-Hill, 1975.Google Scholar
  10. [10]
    Wos, L., Automated Reasoning, American Mathematical Monthly, Vol. 92,No.2, Feb. 1985.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1990

Authors and Affiliations

  • Li Dafa
    • 1
  1. 1.Dept. of Applied MathematicsTsinghua UniversityBeijingChina

Personalised recommendations