@inproceedings{10.1007/978-3-540-30124-0_3,
    Abstract = {A Craig interpolant [1] for a mutually inconsistent pair of formulas (A,B) is a formula that is (1) implied by A, (2) inconsistent with B, and (3) expressed over the common variables of A and B. It is known that a Craig interpolant can be efficiently derived from a refutation of A ∧ B, for certain theories and proof systems. For example, interpolants can be derived from resolution proofs in propositional logic, and for ``cutting planes'' proofs for systems of linear inequalities over the reals [5,3]. These methods have been extended to the theory of linear inequalities with uninterpreted function symbols [4].},
    Address = {Berlin, Heidelberg},
    Author = {McMillan, Kenneth},
    BookTitle = {Computer Science Logic},
    Editor = {Marcinkowski, Jerzy and Tarlecki, Andrzej},
    File = {Applications of Craig Interpolation to Model Checking - a - a - a - w.pdf},
    ISBN = {978-3-540-30124-0},
    Pages = {22--23},
    Publisher = {Springer Berlin Heidelberg},
    Title = {Applications of Craig Interpolation to Model Checking},
    Year = {2004},
    date-added = {2020-02-29 18:26:29 +0100},
    date-modified = {2020-02-29 18:26:29 +0100},
    doi = {10.1007/978-3-540-30124-0_3}
}

@inproceedings{10.1007/978-3-540-30124-0_3, Abstract = {A Craig interpolant [1] for a mutually inconsistent pair of formulas (A,B) is a formula that is (1) implied by A, (2) inconsistent with B, and (3) expressed over the common variables of A and B. It is known that a Craig interpolant can be efficiently derived from a refutation of A ∧ B, for certain theories and proof systems. For example, interpolants can be derived from resolution proofs in propositional logic, and for ``cutting planes'' proofs for systems of linear inequalities over the reals [5,3]. These methods have been extended to the theory of linear inequalities with uninterpreted function symbols [4].}, Address = {Berlin, Heidelberg}, Author = {McMillan, Kenneth}, BookTitle = {Computer Science Logic}, Editor = {Marcinkowski, Jerzy and Tarlecki, Andrzej}, File = {Applications of Craig Interpolation to Model Checking - a - a - a - w.pdf}, ISBN = {978-3-540-30124-0}, Pages = {22--23}, Publisher = {Springer Berlin Heidelberg}, Title = {Applications of Craig Interpolation to Model Checking}, Year = {2004}, date-added = {2020-02-29 18:26:29 +0100}, date-modified = {2020-02-29 18:26:29 +0100}, doi = {10.1007/978-3-540-30124-0_3} }