Interpolation and symbol elimination

Laura Kovács, Andrei Voronkov

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    We prove several results related to local proofs, interpolation and superposition calculus and discuss their use in predicate abstraction and invariant generation. Our proofs and results suggest that symbol-eliminating inferences may be an interesting alternative to interpolation. © 2009 Springer Berlin Heidelberg.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    PublisherSpringer Nature
    Pages199-213
    Number of pages14
    Volume5663
    ISBN (Print)3642029582, 9783642029585
    DOIs
    Publication statusPublished - 2009
    Event22nd International Conference on Automated Deduction, CADE-22 - Montreal, Canada
    Duration: 2 Aug 20097 Aug 2009

    Publication series

    NameLecture Notes in Computer Science

    Conference

    Conference22nd International Conference on Automated Deduction, CADE-22
    Country/TerritoryCanada
    CityMontreal
    Period2/08/097/08/09

    Fingerprint

    Dive into the research topics of 'Interpolation and symbol elimination'. Together they form a unique fingerprint.

    Cite this