Sciweavers

COCOON
1995
Springer

Constructing Craig Interpolation Formulas

14 years 2 months ago
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.
Guoxiang Huang
Added 25 Aug 2010
Updated 25 Aug 2010
Type Conference
Year 1995
Where COCOON
Authors Guoxiang Huang
Comments (0)