Posted By: valkiriC'est qui BOZOO?

Un mec avec un gros nez rouge et un chapeau qui bouge non mais enfin tout le monde sait ca!

Posted By: Puyo Puyo[/citetu es sûre de toi Mélanie ?

Amelie!

Posted By: Puyo PuyoDis dons Amélie, je me disais un truc...

ouai, quoi? tu veux que je fasse la preuve d'une troisieme autre maniere peut etre?

Posted By: parasiteC'est quoi une preuve? une épreuve sans le "é"?

C'est ça:

\begin{proof}
(i) was shown in \cite{walukiewicz} and the three other
completeness results might actually be derivable from it. But
direct (and simpler) proofs for (ii) and (iii) can be found
respectively in \cite{kaivola} and
\cite{DBLP:conf/fossacs/CateF10}. As regards (iv), first remark
that $K_\mu~+~\lozenge \varphi \leftrightarrow \Box \varphi$ is
equivalent to $K_\mu~+~\lozenge \varphi \rightarrow \Box
\varphi~+~\Box \varphi \rightarrow \lozenge \varphi$. Then, let us
show the following. Let $\xi$ be derivable in $K_\mu~+~\lozenge
\varphi \rightarrow \Box \varphi~+~\Box \varphi \rightarrow
\lozenge \varphi$, then $\neg(\mu x. \Box x)\rightarrow \xi$ is
derivable in $K_\mu~+~\lozenge \varphi \rightarrow \Box \varphi$.
The proof goes by induction on the length of the $K_\mu~+~\lozenge
\varphi \rightarrow \Box \varphi~+~\Box \varphi \rightarrow
\lozenge \varphi$-proof. Assume the proof is of length $1$, then
$\xi$ is an axiom. If it is not the $\Box \varphi \rightarrow
\lozenge \varphi$ axiom, then it is also a $K_\mu~+~\lozenge
\varphi \rightarrow \Box \varphi$-proof. Otherwise, notice that
$\Box \bot \rightarrow \mu x. \Box x$ is valid in the
$\mu$-calculus, which yields $\vdash \Box (\varphi \wedge \neg
\varphi) \rightarrow \mu x. \Box x$, i.e., $\vdash (\Box \varphi
\wedge \Box \neg \varphi) \rightarrow \mu x. \Box x$ ($\Box$
distributing over conjunction), i.e., $\vdash \neg (\Box \varphi
\rightarrow \lozenge \varphi) \rightarrow \mu x. \Box x$, i.e.,
$\vdash \neg (\mu x. \Box x) \rightarrow (\Box \varphi \rightarrow
\lozenge \varphi)$ and so this is also derivable in
$K_\mu~+~\lozenge \varphi \rightarrow \Box \varphi$. Now assume
the property holds for all $K_\mu~+~\lozenge \varphi \rightarrow
\Box \varphi~+~\Box \varphi \rightarrow \lozenge \varphi$-proofs
of length $n$. Consider now a formula with a proof of length
$n+1$. If the last rule is the Modus Ponens, then the property
simply follows by propositional logic. So assume the last rule is
the necessitation rule and $\xi$ is of the form $\Box \theta$. By
induction hypothesis, there is a $K_\mu~+~\lozenge \varphi
\rightarrow \Box \varphi$-proof of $\neg(\mu x.\Box x)\rightarrow
\theta$. By contraposition, we get $\vdash \neg \theta \rightarrow
(\mu x.\Box x)$ and by necessitation, $K$ and propositional
tautologies, $\vdash \Box \neg \theta \rightarrow \Box (\mu x.\Box
x)$. As by the fixpoint axiom, $\vdash \Box (\mu x. \Box x)
\rightarrow \mu x. \Box x$, then also by propositional tautologies
$\vdash \Box \neg \theta \rightarrow \mu x. \Box x$. By
contraposition we obtain $\vdash \neg (\mu x. \Box x) \rightarrow
\neg \Box \neg \theta$. By the $\lozenge \phi \rightarrow \Box
\phi$ axiom, it follows that $\vdash \neg (\mu x. \Box x)
\rightarrow \Box \theta$. Finally, assume the last rule is the
fixpoint rule and $\xi$ is of the form $\mu y. \theta \rightarrow
\psi$. By induction hypothesis, $\vdash \neg(\mu x. \Box
x)\rightarrow(\theta[y / \psi] \rightarrow \psi)$, hence by
propositional tautologies $\vdash (\neg(\mu x. \Box x)\rightarrow
\theta[y / \psi]) \rightarrow (\neg(\mu x. \Box
x)\rightarrow\psi)$, i.e., $\vdash (\neg(\mu x. \Box
x)\rightarrow\theta)[y / \psi] \rightarrow (\neg(\mu x. \Box
x)\rightarrow\psi)$. By the fixpoint rule it follows that
$\vdash \mu y. (\neg(\mu x. \Box
x)\rightarrow\theta) \rightarrow (\neg(\mu x. \Box
x)\rightarrow\psi))$. By propositional tautologies, $\vdash \mu y. (\neg(\mu x. \Box
x)\rightarrow(\theta \rightarrow \psi))$.
It follows that $\vdash \neg(\mu x. \Box
x)\rightarrow (\mu y. \theta \rightarrow \psi)$ (as the two formulas are equivalent in the $\mu$-calculus).
Now let us rely on \cite{DBLP:conf/fossacs/CateF10}, where it is
shown that if $\psi$ is valid on finite words, then $\mu x. \Box x
\rightarrow \psi$ is derivable in $K_\mu~+~\lozenge \theta
\rightarrow \Box \varphi$. We now have that if $\psi$ is valid on
finite and $\omega$-words, then $\mu x. \Box x \rightarrow \psi$
and $\neg (\mu x. \Box x) \rightarrow \psi$ are both derivable in
$K_\mu~+~\lozenge \theta \rightarrow \Box \varphi$ and so $\psi$ is also $K_\mu~+~\lozenge \theta \rightarrow \Box \varphi$-derivable.
\end{proof}

Ouai, c'est dégueulasse. Et ça empêche de dormir, et de manger. Et il me semble que c'est encore assez imprécis. Et en plus, ça c'est une petite preuve de rien du tout, imagine quand ça fait 30 pages..

Posted By: valkiriCQFD

elle est fausse :pin05:
je tente la méthode numéro 74.. et après je me suicide

Posted By: valkiriJ'ai mal a la tete!

A qui le dis-tu!!!! J'en peux plus :pin06:

\begin{proof}
(i) was shown in \cite{walukiewicz} and the three other
completeness results might actually be derivable from it. But
direct (and simpler) proofs for (ii) and (iii) can be found
respectively in \cite{kaivola} and
\cite{DBLP:conf/fossacs/CateF10}. In order to establish (iv), we will rely on (i), (ii) and (iii). We first show the following claim:
\begin{itemize}
\item \emph{Claim: Let $K_x$ be a system extending $K_\mu$ with a finite set of axioms and closed under Substitution, Modus Ponens and the fixpoint and Necessitation rules. Let $\theta$ be a formula with $K_x \vdash \theta \rightarrow \Box \theta$.
For all formulas $\xi$, if $K_x ~+~ \theta \vdash \xi$, then $K_x \vdash \theta \rightarrow \xi$.}\\
The proof goes by induction on the length of $K_x$-derivations. The only difficult case is whenever the last line in the proof is obtained via the application of the fixpoint rule. So assume the property holds for all derivations of length $n$ and
$K_x ~+~ \theta \vdash \mu y. \phi \rightarrow \psi$ is the last line of a derivation of length $n+1$. We want to show that $K_x \vdash \theta \rightarrow (\mu y. \phi \rightarrow \psi)$.
By induction hypothesis, $K_x\vdash\theta \rightarrow (\phi[x/\psi] \rightarrow \psi)$. So by propositional tautologies
also $K_x \vdash (\theta \wedge \phi[\psi/x]) \rightarrow \psi$. By the fixpoint rule, $K_x \vdash \mu x.(\theta \wedge \phi) \rightarrow \psi$.
But given that it is valid in the $\mu$-calculus that $\theta \rightarrow \Box^* \theta$ (where $\Box^*$ is the transitive closure of the $\Box$ operator), we can also prove in the $\mu$-calculus that $\theta \rightarrow (\mu x.(\theta \wedge \phi) \leftrightarrow \mu x.\phi)$.
It follows that $K_x \vdash \theta \rightarrow(\mu x.\phi \rightarrow \psi)$.
\end{itemize}
Now assume that $\xi$ is valid on finite and $\omega$-words.
As it is valid on finite words, by (iii), $ K_\mu ~+~ \lozenge \phi \rightarrow \Box \phi ~+~ \mu x.\Box x \vdash \xi$. As $\mu x.\Box x$
satisfies the condition of the claim we get:
\begin{center}
(a) $K_\mu~+~\lozenge \phi \rightarrow \Box \phi \vdash \mu x.\Box x \rightarrow \xi$
\end{center}
$\xi$ is also valid on $\omega$-words, and hence by (ii), $K_\mu ~+~ \lozenge \phi \rightarrow \Box \phi ~+~ \Box \phi \rightarrow \lozenge \phi \vdash \xi$. Note that $\lozenge \top$ can equivalently be substituted for $\Box \phi \rightarrow \lozenge \phi$ there. As
$K_\mu ~+~ \lozenge \phi \rightarrow \Box \phi \vdash \neg \mu x.\Box x \rightarrow \lozenge \top$, we can also take $\theta$ to be $\neg\mu x.\Box x$, which also satisfies the condition of the claim. Indeed by the $\lozenge \phi \rightarrow \Box \phi$ axiom, it is enough to prove $\neg \mu x.\Box x \rightarrow \lozenge \neg \mu x.\Box x$.
But this is equivalent to $\Box \mu x.\Box x \rightarrow \mu x.\Box x$, which is
derivable in $K_\mu$ (since $\mu x.\Box x \leftrightarrow \Box(\mu x.\Box x)$).
It follows that:
\begin{center}
(b) $K_\mu~+~\lozenge \phi \rightarrow \Box \phi \vdash \neg (\mu x.\Box x) \rightarrow \xi$
\end{center}
$K_\mu~+~\lozenge \phi \rightarrow \Box \phi \vdash \xi$ follows from (a) and (b), which proves (iv).

T'en es où de ton controle de soft de 3D parametrique avec ton controleur midi Valkiri?

Bin moi la suis rentré chez moi, je reprends ca lundi. Ca marche pas encore mais c'est en bonne voie : le tout est d'envoyer des données UDP vers processing, intégré à grasshopper (deja ca c'est chaud à intégrer) qui lui-meme est intégré en tant que plugin dans rhinoceros. Les données UDP (User Datagram Protocol) vont venir soit de processing lui-même, mais pour l'instant j'arrive pas à le faire prendre les données venant du controleur, soit de pure data ou la j'arrive à capter les signaux, mais pas à les envoyer en UDP vers processing...
Dans la semaine je pense y arriver. Ce qui fait peur c'est que le developpeur de grasshopper lui-même n'a aucune idée de comment faire, il ne s'est encore pas du tout intéressé au midi (un pote l'a contacté a ce sujet).

Pourtant un gars a bien réussi à le faire, mais passe a priori par Arduino.
Voici son exemple :
http://www.youtube.com/watch?v=WYcriR227Dg

En fait avec des potes on s'interresse serieusement à grasshopper car c'est comme pure data ou reaktor, mais pour la 3D. Tu fais une tour de dingue trop belle avec tout le calpinage de facade (et +) en 5min, une fois le systeme créé (ce qui prend du temps ca par contre). Du process quoi.
Et c'est ca d'ailleurs dont je voulais te parler. Ca en devient de la logique pure :pin01:

Mais bon d'ici 2-3 semaines on sera + au fait des possibilités.
Voici quelques exemples de 3D parametrique chopés la vite fait :
http://www.youtube.com/watch?v=V9BesCa5K5k&feature=related
http://www.youtube.com/watch?v=QhV0J-EW8Eg&feature=related
http://www.youtube.com/watch?v=qBhsh7PVyo0&feature=related
http://www.youtube.com/watch?v=6N6WokSWBbc&feature=related

La ca commence a devenir + intéressant :
http://www.youtube.com/watch?v=LJUo3iPF-5E&feature=related
http://www.youtube.com/watch?v=GCnCL05n91g&feature=related

Et pour finir, un exemple d'archi qui fait du parametrique (je ne mets qu'elle alors que y'en a pas mal et c'est pas la + interessante, mais c'est une femme, ancienne mathématicienne donc pour le coup ^^) : Zaha Hadid

Posted By: valkiri bien que n'ayant pas pratiqué depuis longtemps hum :)

ah ouai, moi aussi: ça fait 8 ans!