Passer au contenu principal

Recherche

Afficher tous les résultats pour

Accueil

Publication

Interpolation and Symbol Elimination

À propos
Confidentialité
Mentions légales

Copyright © 2025 EPFL, tous droits réservés

Graph Chatbot

Laura Ildiko Kovacs
2009

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/entities/publication/f3be429c-28ed-4b98-9d8a-78922e6d3618

À 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.

Concepts associés (25)

Interpolation numérique

En analyse numérique (et dans son application algorithmique discrète pour le calcul numérique), l'interpolation est une opération mathématique permettant de remplacer une courbe ou une fonction par une autre courbe (ou fonction) plus simple, mais qui coïncide avec la première en un nombre fini de points (ou de valeurs) donnés au départ. Suivant le type d'interpolation, outre le fait de coïncider en un nombre fini de points ou de valeurs, il peut aussi être demandé à la courbe ou à la fonction construite de vérifier des propriétés supplémentaires.

Interpolation multivariée

En analyse numérique, linterpolation multivariée ou linterpolation spatiale désigne l'interpolation numérique de fonctions de plus d'une variable. Le problème est similaire à celui de l'interpolation polynomiale sur un intervalle réel : on connait les valeurs d'une fonction à interpoler aux points et l'objectif consiste à évaluer la valeur de la fonction en des points . L'interpolation multivariée est notamment utilisée en géostatistique, où elle est utilisée pour reconstruire les valeurs d'une variable régionalisée sur un domaine à partir d'échantillons connus en un nombre limité de points.

Interpolation polynomiale

En mathématiques, en analyse numérique, l'interpolation polynomiale est une technique d'interpolation d'un ensemble de données ou d'une fonction par un polynôme. En d'autres termes, étant donné un ensemble de points (obtenu, par exemple, à la suite d'une expérience), on cherche un polynôme qui passe par tous ces points, p(xi) = yi, et éventuellement vérifie d'autres conditions, de degré si possible le plus bas. Cependant, dans le cas de l'interpolation lagrangienne, par exemple, le choix des points d'interpolation est critique.

Publications associées (28)

SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus

Motivated by the transfer of proofs between proof systems, and in particular from first order automated theorem provers (ATPs) to interactive theorem provers (ITPs), we specify an extension of the TPTP derivation text format to describe proofs in first-ord ...

2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in orthologic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based pro ...

Springer International Publishing Ag2024

Interpolation and Quantifiers in Ortholattices

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We study quantifiers and interpolation properties in ortho- logic, a non-distributive weakening of classical logic that is sound for formula validity with respect to classical logic, yet has a quadratic-time decision procedure. We present a sequent-based p ...

2024