Constructing Craig interpolation formulas

  • Guoxiang Huang
Session 3B: Distributed/Logic
Part of the Lecture Notes in Computer Science book series (LNCS, volume 959)


A Craig interpolant of two inconsistent theories is a formula which is true in one and false in the other. This paper gives an efficient method for constructing a Craig interpolant from a refutation proof which involves binary resolution, paramodulation, and factoring. This method can solve the machine learning problem of discovering a first order concept from given examples. It can also be used to find sentences which distinguish pairs of nonisomorphic finite structures.


Interpolation Algorithm Relational Symbol Binary Resolution Atomic Sentence Maximal Occurrence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Roger Lyndon, Notes on Logic, D. Van Nostrand Company, Princeton, 1966.Google Scholar
  2. 2.
    Chin-Liang Chang, Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.Google Scholar
  3. 3.
    C C. Chang, H. Jerome Keisler, Model Theory, North Holland, 1990.Google Scholar
  4. 4.
    Larry Wos, Overbeek, Lusk, Boyle, Automated Reasoning: Introduction and Applications, McGraw-Hill, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Guoxiang Huang
    • 1
  1. 1.Mathematics DepartmentUniversity of Hawaii at ManoaHonolulu

Personalised recommendations