Constructing Craig Interpolation Formulas

A Craig interpolant of two inconsistent theories is a formula which is true in one and false in the other. This paper gives an eificient 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.

• Type: Conference
• Year: 1995
• Where: COCOON
• Authors: Guoxiang Huang
• Keywords: COCOON 1995, Combinatorics, Craig Interpolant, Inconsistent Theories, Machine Learning Problem