Commencer une discussion
Annoncer un événement
Proposer une release
🍍 Ananas It !En savoir plus
Une discussion au hasard !
TV Incongrue
Zap! | Plein écran
Pinacothèque
Alternatives
Voir la galerie de la discussion
Vanilla 1.3.0 is a product of Lussumo. More Information: Documentation, Community Support.
Ce que vous allez trouver ici :
- Des discussions plus ou moins inspirées (car nous sommes bien sur un forum)
- Un calendrier d'évènements, pour vous aider à occuper vos soirées
- La liste exhaustive de toutes les sorties musicales annoncées sur ce forum depuis sa création
- Une radio automatique et surprenante
- Une pinacothèque collaborative
Cerise sur le gâteau, vous pouvez très facilement apporter votre contribution à tout ça. Pour ce faire, le mieux est encore de vous connecter ou de vous inscrire :)
Enfin, vous pouvez nous contacter directement à l'adresse email : contact (CHEZ) musiques-incongrues (POINT) net
-
-
CommentAuthorPascal Lebrain
- CommentTimeJun 24th 2010 edited
Hé cool Johan ! Ça fait un bail qu'on t'attend ! :pin01:
-
-
ah ba c'est pas trop tot:pin01::pin01:
-
C'est qui BOZOO?
-
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!
-
-
CommentAuthorPascal Lebrain
- CommentTimeJun 24th 2010
Le nez m'a l'air normal... pas de chapeau... tu es sûre de toi Mélanie ?
-
-
ouai parfois il se deguise aussi
-
Tout ca en écoutant "Christer Bladin - Wildkatze" sur musique approximative c'est beau :pin01:
-
Posted By: Puyo Puyo[/citetu es sûre de toi Mélanie ?
Amelie! -
tout ca en etant partagee entre mes deux superviseurs dont l'un envoie un mail qui dit:
"non fait la preuve comme ca"
et l'autre:
"non comme ca d'abord"
l'un:
"moi d'abord!"
l'autre:
"moi d'abord"
non mais je vous jure... -
-
CommentAuthorPascal Lebrain
- CommentTimeJun 24th 2010
Oui oui Emilie, t'énerves pas :pin01:
-
-
Oui Rascal :pin01:
-
-
CommentAuthorPascal Lebrain
- CommentTimeJun 24th 2010
Dis dons Amélie, je me disais un truc...
-
-
Ah non bin me suis pas trompé haha
-
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?
-
-
CommentAuthorPascal Lebrain
- CommentTimeJun 24th 2010
Non, c'était juste pour m'habituer à dire Amélie hé hé
-
-
Cool, j'ai eu peur! :pin01: parce que j'en peux plus la.. :pin06:
-
C'est quoi une preuve? une épreuve sans le "é"?
-
-
CommentAuthorAntiulcéreuse
- CommentTimeJun 25th 2010
Stop la philo.
-
-
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..
-
CQFD
-
Posted By: valkiriCQFD
elle est fausse :pin05:
je tente la méthode numéro 74.. et après je me suicide -
On va pouvoir faire un suicide collectif. Depuis ce matin j'essaie de controler un soft de 3D parametrique avec mon controleur midi. J'ai fait du C#, du pure data, du maxmsp, et la je me lance dans processing. J'ai mal a la tete!
-
Posted By: valkiriJ'ai mal a la tete!
A qui le dis-tu!!!! J'en peux plus :pin06:
-
:pin02::pin02::pin02:OUAI!!!:pin02::pin02::pin02:
\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?
-
Ah bin voila c'etait si simple ;)
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=WYcriR227DgEn 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=relatedLa ca commence a devenir + intéressant :
http://www.youtube.com/watch?v=LJUo3iPF-5E&feature=related
http://www.youtube.com/watch?v=GCnCL05n91g&feature=relatedEt 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
-
-
CommentAuthorAntiulcéreuse
- CommentTimeJun 25th 2010
Ton projet marche peut-être mais j'ai suivi tes conseils pour un ventilateurs humain DIY sous créative commons, ça marche bien.
-
-
:grapp01:
-
Ca m'a l'air plutôt chouette Grasshopper :pin01: moi par contre je suis en info très très théorique, maintenant je vais commencer à faire des bases de données et du xml (entendons-nous bien: des maths applicables aux bases de données et à xml), mais je panique quand même dès que je vois écrit "peer to peer" ou "data stream sampling", alors là mon boss me rassure et me dis que mais non c'est des maths :pin01: donc je ne sais pas si je pourrai comprendre vos trucs de 3D ou aider en quoi que ce soit, mais je serai curieuse d'en discuter, de toutes façons j'ai décidé qu'il fallait que je m'améliore et que je m'ouvre au monde des nouvelles technologies :grapp01: (à vrai dire j'ai plus trop le choix, va bien falloir que je fasse cours en info et y a pas que des cours de logique en info et.. oui.. faudrait aussi que je passe à linux)
-
Et sinon BOZOO il en pense quoi lui d'abord?
-
je commence à être une machine à produire de la récurrence, c'est pas mal utile quand on code je crois bien, par contre j'ai très rarement fait ça (coder) et je déteste viscéralement Java (sale, moche, pas élégant: beurk) et j'ai un peu la flemme d'apprendre la syntaxe de langages que je connais pas, mais faut voir ouai :grapp01: moi j'aime Lisp http://en.wikipedia.org/wiki/Lisp_%28programming_language%29
-
Oui!!! On en avait parlé l'autre fois...je suis fan du Lisp, bien que n'ayant pas pratiqué depuis longtemps hum :)
-
Posted By: valkiri bien que n'ayant pas pratiqué depuis longtemps hum :)
ah ouai, moi aussi: ça fait 8 ans!
-
eh valk pourquoi t'utilise pas OSC pour faire communiquer puredata et processing ?
-
-
CommentAuthorPascal Lebrain
- CommentTimeJun 26th 2010
En tous cas cette discussion est une épreuve pour moi. :pin01:
-
1 to 34 of 34