Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Dependence logic
Summary
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.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related lectures (1)