Publication

Interpolation and Symbol Elimination

2009
Conference Papers

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

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

2009
Conference Papers

Résumé

Source officielle

Concepts associés (31)

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.

Règle d'inférence

Dans un système logique, les régles d'inférence sont les règles qui fondent le processus de déduction, de dérivation ou de démonstration. L'application des règles sur les axiomes du système permet d'en démontrer les théorèmes. Une règle d'inférence est une fonction qui prend un -uplet de formules et rend une formule. Les formules arguments sont appelées « les prémisses » et la formule retournée est appelée la « conclusion ».

Afficher plus

Publications associées (31)

Afficher plus

Interpolation and Symbol Elimination

Chattez avec Graph Search

Interpolation and Quantifiers in Ortholattices

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

Orthologic with Axioms