Publication

Sets with Cardinality Constraints in Satisfiability Modulo Theories

Concepts associés (41)

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

Second-order logic

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).

Complete Boolean algebra

In mathematics, a complete Boolean algebra is a Boolean algebra in which every subset has a supremum (least upper bound). Complete Boolean algebras are used to construct Boolean-valued models of set theory in the theory of forcing. Every Boolean algebra A has an essentially unique completion, which is a complete Boolean algebra containing A such that every element is the supremum of some subset of A. As a partially ordered set, this completion of A is the Dedekind–MacNeille completion.

Satisfaisabilité

En logique mathématique, la satisfaisabilité ou satisfiabilité et la validité sont des concepts élémentaires de sémantique. Une formule est satisfaisable s'il est possible de trouver une interprétation (modèle), une façon d'interpréter tous les éléments constitutifs de la formule, qui rend la formule vraie. Une formule est universellement valide, ou en raccourci valide si, pour toutes les interprétations, la formule est vraie.

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.

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.

Formule logique

En logique on dit d’une suite finie de lettres qu’elle est une formule, ou parfois formule bien formée, d'un langage logique donné lorsqu’elle peut être construite en appliquant une combinaison des règles de la grammaire formelle associée, on parle de la syntaxe du langage. Informellement les formules sont les assemblages de lettres auxquels il est possible de donner une signification en termes de valeur de vérité (Vrai, ou Faux). Les formules logiques sont l'équivalent des phrases du langage naturel.

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.

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.

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.

Anneau de Boole

Un anneau de Boole (ou Algèbre de Boole), est un anneau unitaire (E, +, •, 0, 1) dans lequel tout élément a vérifie la relation a•a = a. Il découle immédiatement de la définition qu'un anneau de Boole est commutatif et que chaque élément est son propre opposé (en calculant le carré de x + 1, puis celui de x + y). En un sens qui peut être rendu précis, les anneaux de Boole sont les algèbres de Boole présentées autrement.