Publication

Polite Combination in Parametric Array Theories

2025

Résumé

Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We observe that decision procedures for the satisfiability of these theories rely on a kind of finite witnessability property. We use this insight to show the politeness of these theories with respect to the index and element sorts. Our results clarify the politeness of the theory of sets with the cardinality operator, which was left open in the literature.

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.

2025

Résumé

Source officielle

Concepts associés (32)

Théorie

Une théorie (du grec theoria, « contempler, observer, examiner ») est un ensemble cohérent, si elle prétend à la scientificité, d'explications, de notions ou d'idées sur un sujet précis, pouvant inclure des lois et des hypothèses, induites par l'accumulation de faits provenant de l'observation, l'expérimentation ou, dans le cas des mathématiques, déduites d'une base axiomatique donnée : théorie des matrices, des torseurs, des probabilités.

Théorie des modèles

La théorie des modèles est une branche de la logique mathématique qui traite de la construction et de la classification des structures. Elle définit en particulier les modèles des théories axiomatiques, l'objectif étant d'interpréter les structures syntaxiques (termes, formules, démonstrations...) dans des structures mathématiques (ensemble des entiers naturels, groupes, univers...) de façon à leur associer des concepts de nature sémantique (comme le sens ou la vérité).

Tri à bulles

vignette|Visualisation statique du tri : les étapes vont de gauche à droite. À chaque étape une permutation est faite. La couleur la plus foncée a le plus de valeur et trouve sa place définitive (en bas) en premier. Le tri à bulles ou tri par propagation est un algorithme de tri. Il consiste à comparer répétitivement les éléments consécutifs d'un tableau, et à les permuter lorsqu'ils sont mal triés. Il doit son nom au fait qu'il déplace rapidement les plus grands éléments en fin de tableau, comme des bulles d'air qui remonteraient rapidement à la surface d'un liquide.

Afficher plus

Publications associées (15)

Afficher plus

Polite Combination in Parametric Array Theories

Chattez avec Graph Search

Unpacking the Sharing Economy: From Participation to Impact

On Counter-Example Complete Verification for Higher-Order Functions

On Cafesat: A Modern SAT Solver for Scala