Publication

Polite Combination in Parametric Array Theories

2025

Abstract

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.

Official source

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2025

Abstract

Official source

Related concepts (32)

Theory

A theory is a rational type of abstract thinking about a phenomenon, or the results of such thinking. The process of contemplative and rational thinking is often associated with such processes as observational study or research. Theories may be scientific, belong to a non-scientific discipline, or no discipline at all. Depending on the context, a theory's assertions might, for example, include generalized explanations of how nature works. The word has its roots in ancient Greek, but in modern use it has taken on several related meanings.

Model theory

In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the statements of the theory hold). The aspects investigated include the number and size of models of a theory, the relationship of different models to each other, and their interaction with the formal language itself.

Bubble sort

Bubble sort, sometimes referred to as sinking sort, is a simple sorting algorithm that repeatedly steps through the input list element by element, comparing the current element with the one after it, swapping their values if needed. These passes through the list are repeated until no swaps had to be performed during a pass, meaning that the list has become fully sorted. The algorithm, which is a comparison sort, is named for the way the larger elements "bubble" up to the top of the list.

Related publications (15)

Polite Combination in Parametric Array Theories

Chat with 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