Publication

On Sets with Cardinality Constraints in Satisfiability Modulo Theories

Concepts associés (47)

Graph Chatbot

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.

Connectez-vous pour utiliser Chat avec Graph Search

NP-difficile

vignette|300px|Mise en évidence d'un problème NP-difficile si Problème P ≟ NP. Un problème NP-difficile est, en théorie de la complexité, un problème appartenant à la classe NP-difficile, ce qui revient à dire qu'il est au moins aussi difficile que les problèmes les plus difficiles de la classe NP. Ainsi, un problème H est NP-difficile, si tout problème L de la classe NP peut être réduit en temps polynomial à H. Si un problème NP-difficile est dans NP, alors c'est un problème NP-complet.

Generalized algebraic data type

In functional programming, a generalized algebraic data type (GADT, also first-class phantom type, guarded recursive datatype, or equality-qualified type) is a generalization of parametric algebraic data types. In a GADT, the product constructors (called data constructors in Haskell) can provide an explicit instantiation of the ADT as the type instantiation of their return value. This allows defining functions with a more advanced type behaviour.

Type (informatique)

vignette|Présentation des principaux types de données. En programmation informatique, un type de donnée, ou simplement un type, définit la nature des valeurs que peut prendre une donnée, ainsi que les opérateurs qui peuvent lui être appliqués. La plupart des langages de programmation de haut niveau offrent des types de base correspondant aux données qui peuvent être traitées directement — à savoir : sans conversion ou formatage préalable — par le processeur.

Lindström quantifier

In mathematical logic, a Lindström quantifier is a generalized polyadic quantifier. Lindström quantifiers generalize first-order quantifiers, such as the existential quantifier, the universal quantifier, and the counting quantifiers. They were introduced by Per Lindström in 1966. They were later studied for their applications in logic in computer science and database query languages. In order to facilitate discussion, some notational conventions need explaining.

Universal quantification

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Décidabilité

En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique. L’indécidabilité est la négation de la décidabilité. Dans les deux cas, il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique. Une proposition (on dit aussi énoncé) est dite décidable dans une théorie axiomatique si on peut la démontrer ou démontrer sa négation dans le cadre de cette théorie.

Type récursif

En programmation informatique et théorie des types, un type récursif est un type de données dont la définition fait appel au type lui‐même, de façon récursive. Cela permet entre autres des structures de données qui contiennent des sous‐structures du même type. Cette notion s'applique naturellement dans l'étude des listes et des arbres. Type algébrique de données Les types algébriques sont de loin la forme la plus courante de types récursifs. Un exemple classique est le type liste.

Dependence logic

Dependence logic is a logical formalism, created by Jouko Väänänen, which adds dependence atoms to the language of first-order logic. A dependence atom is an expression of the form , where are terms, and corresponds to the statement that the value of is functionally dependent on the values of . Dependence logic is a logic of imperfect information, like branching quantifier logic or independence-friendly logic (IF logic): in other words, its game-theoretic semantics can be obtained from that of first-order logic by restricting the availability of information to the players, thus allowing for non-linearly ordered patterns of dependence and independence between variables.

Independence-friendly logic

Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and Gabriel Sandu in 1989) is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic.

Axiomes de Peano

vignette|Giuseppe Peano En mathématiques, les axiomes de Peano sont des axiomes pour l'arithmétique proposés initialement à la fin du par Giuseppe Peano, et qui connaissent aujourd'hui plusieurs présentations qui ne sont pas équivalentes, suivant la théorie sous-jacente, théorie des ensembles, logique du second ordre ou d'ordre supérieur, ou logique du premier ordre. Richard Dedekind avait proposé une formalisation assez proche, sous une forme non axiomatique.