Interpolation and Symbol Elimination

Laura Ildiko Kovacs
2009
Article de conférence

Résumé

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.

Source officielle

https://infoscience.epfl.ch/record/159235?ln=fr

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Interpolation and Symbol Elimination

Interpolation and Quantifiers in Ortholattices

Interpolation and Quantifiers in Ortholattices

Computer-assisted proof of kernel inequalities

Interpolation and Quantifiers in Ortholattices

Interpolation and Quantifiers in Ortholattices

Computer-assisted proof of kernel inequalities