Constructing Craig interpolation formulas
- 165 Downloads
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.
KeywordsInterpolation Algorithm Relational Symbol Binary Resolution Atomic Sentence Maximal Occurrence
Unable to display preview. Download preview PDF.
- 1.Roger Lyndon, Notes on Logic, D. Van Nostrand Company, Princeton, 1966.Google Scholar
- 2.Chin-Liang Chang, Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.Google Scholar
- 3.C C. Chang, H. Jerome Keisler, Model Theory, North Holland, 1990.Google Scholar
- 4.Larry Wos, Overbeek, Lusk, Boyle, Automated Reasoning: Introduction and Applications, McGraw-Hill, 1992.Google Scholar