Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Dependence logic
Résumé
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. However, dependence logic differs from these logics in that it separates the notions of dependence and independence from the notion of quantification.
The syntax of dependence logic is an extension of that of first-order logic. For a fixed signature σ = (Sfunc, Srel, ar), the set of all well-formed dependence logic formulas is defined according to the following rules:
Terms in dependence logic are defined precisely as in first-order logic.
There are three types of atomic formulas in dependence logic:
A relational atom is an expression of the form for any n-ary relation in our signature and for any n-tuple of terms ;
An equality atom is an expression of the form , for any two terms and ;
A dependence atom is an expression of the form , for any and for any n-tuple of terms .
Nothing else is an atomic formula of dependence logic.
Relational and equality atoms are also called first-order atoms.
For a fixed signature σ, the set of all formulas of dependence logic and their respective sets of free variables are defined as follows:
Any atomic formula is a formula, and is the set of all variables occurring in it;
If is a formula, so is and ;
If and are formulas, so is and ;
If is a formula and is a variable, is also a formula and .
Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.