Wer Fragen wie „Wird OpenSource verboten?“ hört, könnte meinen ich übertreibe völlig und würde antworten: „Nein, es wird nur irgendwas geändert, was nicht in deine verbohrte Ideologie passt, du Kommunist!!1!“. Ich hoffe natürlich, dass meine Befürchtungen übertrieben sind und OpenSource legal bleibt. Im Folgenden will ich jedoch erläutern, warum ich glaube, dass die EU-Kommission und das Landgericht Hamburg zur Zeit zu den Totengräbern der quelloffenen Software werden könnten.

„Fair Search“ findet Android unfair

Beginnen möchte ich mit einer Entscheidung, die die EU-Kommission demnächst treffen wird. Die einzige Quelle hierzu ist zur Zeit die „Financial Times“, die behauptet Quellen zu haben, wonach die EU die Rechtsmäßigkeit von Android prüft. Wahrscheinlich geht es um eine Kartellbeschwerde einer Organisation namens „Fair Search Europe“.

Was ist eigentlich „Fair Search Europe“?

Bei dem klangvollen Namen „Fair Search“ und der zugehörige Webseite, lässt sich diese Organisation leicht für eine Bürgerrechtsbewegung halten, die das edle Ziel hat, Google fairer zu machen. Die Organisation folgt jedoch dem bewährten Prinzip einen von der Wirtschaft finanzierten Lobbyverband als Bewegung von Bürgern erscheinen zu lassen.

Hinter der genannten Organisation stehen Firmen wie Orcale, Microsoft und Nokia. Nicht nur Verschwörungstheoretiker würden annehmen, dass besagte Firmen hier nicht einfach aus edlen Motiven heraus handeln, sondern slichtweg eine konkurrierendes Mobilbetriebssystem ausschalten wollen.

Was ist an Android unfair?

Interessanter als die Herkunft der Kartellbeschwerde ist das benutzte Argument: Die Firmen beklagen sich, dass Google Android missbraucht, um eigene Dienste (Suchmaschine, Videoplattform, Navigationsdienst …) prominent zu platzieren und zu bewerben. Dies ist eine ähnliche Argumentation, wie sie schon mehrfach gegen Microsoft verwendet wurde, weil etwa „MSN“ oder der „Internet Explorer“ zu eng mit dem sog. Betriebssystem „Windows“ verwoben waren und dadurch beworben wurden.

Anders als Windows ist Android jedoch vorwiegend quelloffen. Daher ist es letztlich die Entscheidung des Herstellers des Mobilgerätes, ob die Dienste des Konzerns aus Mountainview aktiv beworben werden. Ganz böse Zungen würden sogar behaupten, dass viele Hersteller bewusst auf die Dienste von Google setzten, da Kunden genau dies erwarten und verwenden wollen.

Da nun offenbar nicht der Microsoft-Fall vorliegt, betont „Fair Search Europe“ einen weiteren Punkt: Google bietet Android „zu marktunüblichen Preisen“ an.

Ist OpenSource Freeware?

Wenn jetzt tatsächlich festgestellt wird, dass das kostenlose Verteilen von Android ein Handel zu „marktunüblichen Preisen“ darstellt, dann wäre dies durchaus eine Gefahr für OpenSource an sich.

Würde Google nun den Android Quelltext komplett verschlossen halten und manchen Herstellern Android als ausführbares Programm zur undurchsichtigen Bedingungen verteilen, wie es etwa bei Freeware der Fall ist, fände ich dies durchaus bedenklich. OpenSource grenzt sich in meinen Augen jedoch in zwei Punkten von Freeware ab:

Zum Einen lässt sich der Entwicklungsaufwand bei OpenSource dramatisch durch die Verwendung von vorhandenem und von der Gemeinschafte beigetragenem Quelltext enorm reduzieren. Im Extremfall stellt der Anbieter von quelloffene Software nur vorhandene Projekte mit wenig Aufwand zusammen, weswegen von einer Abgabe unter Wert gar nicht gesprochen werden kann. (Sofern der Wert der Arbeitsaufwand des Anbieters ist)

Zum Anderen wird bei OpenSource gar nicht der Quelltext oder das Programm verkauft sondern Dienstleistungen zu der Software. Das wäre etwa so, als würde „Fair Bratwurst Europe“ einen Bratwurststand verklagen, der Senf zu einem marktunüblichen Preis von 0€ zur Bratwurst „verkauft“ .

ProSiebenSat1 klagt gegen quelloffene Downloadverwaltung

Zunächst klingt das Urteil (LG Hambug, Az.: 310 O 144/13) relativ unspektakulär: Eine quelloffene Downloadverwaltung bietet an mit RTMPE „geschützte“ Videos von einer Plattform von ProSiebenSat1 zu sichern, ProSiebenSat1 klagt dagegen und gewinnt vor dem Landgericht Hamburg. Spannend wird das ganze bei Betrachtung der Details:

Beanstandet wurde eine Entwicklerversion. Der fragliche Quelltext wurde aus der Gemeinschaft eingesandt. Der Quelltext wurde gelöscht und hat es nie in eine finale Version geschafft. Dennoch soll die Firma, die das OpenSource-Projekt betreut haftbar gemacht werden..

Eine Gefahr für OpenSource?

Warum ist es nun bedenklich, wenn das Projekt haftbar gemacht wird für fremde Quelltexte, die gleich nach Bekanntwerden gelöscht wurden? Das Problem ist hierbei die Funktionsweise solcher Projekte: Beliebige Entwickler schlagen Quelltet vor; dieser wird präsentiert, geändert und letztendlich angenommen oder abgelehnt. Ist nun der Betreuer des Projekts haftbar für (gelöschte) Zwischenversionen, so führt das dazu, dass der Quelltext im Geheimen eingereicht werden und rechtlich geprüft werden muss, bevor überhaupt öffentlich zur Diskussion gestellt werden. Dies würde sowohl den Entwicklungsprozess verlangsamen als auch die Hemmschwelle für neue Beteiligungen anheben.

Kurz nachdem bekannt war, dass sich Ubuntu auf dem ARM-basierten Smartbook Toshiba AC100 installieren lässt, habe ich mir ein solches Gerät angeschafft. Das ist nun zweieinhalb Jahre her. Seitdem habe ich häufig Ubuntu in vielen Varianten auf das Gerät aufgespielt. Dies war häufig notwendig bei Versionssprüngen. Eigentlich wollte ich an dieser Stelle erzählen, wie schön das inzwischen das Update ohne externes Aufspielen funktioniert. Aus aktuellem Anlass erkläre ich jedoch jetzt, wie sich ein AC100 in wenigen einfachen Schritten zerstören lässt:

1. Zunächst vergessen abootimg als installier zu markieren
2. Die freundliche Frage nach der Aktualiserung der Betriebssystemversion bejahen
3. Die „nicht mehr benötigten“ Pakete (wie abootimg) automatisiert entfernen lassen
4. Neustarten
5. Einen schwarzen Bildschirm anstarren

Lubuntu 13.04 auf dem AC100 installieren

Nachdem ich den schwarzen Bildschirm eine Weile angestarrt habe, ist mir aufgefallen, dass mich diese postmodere Kunst doch nur so mittelschwer anspricht. Also entschied ich mich Lubuntu neuzuinstallieren. Das ist auch nicht so schwer:

• Das Bootimage auf das AC100 spielen
• Einen USB-Stick mit der Installationsdatei einstöpsel
• Anschalten und den Anweisungen folgen
• Die Sicherungskopie des Benutzerverzeichnisses entpacken. (Falls nicht vorhanden, siehe hier)
• Die Tastatureinstellungen anpassen
• Wichtige Pakete wie abootimg und psi-plus installieren

Today after I upgraded the MongoDB connector for NodeJS to the latest version 1.3.9 I encountered strange results with our tests. The ones which use .insert() operations on collections suddenly started to fail because of timeouts. Finally, after some good old caveman debugging I discovered that a callback passed to .insert() was not called anymore, [...]

A step-by-step installation guide to setup a scientific python environment based on Mac OS X and homebrew.

First install homebrew.
Follow their instructions, then come back here.

Have fun

(As always: If you think something is missing leave a comment.)

Because the discussion popped up on the social media.

Structure and Interpretation of Computer Programs, Section 3.5 has an explanation on how you can encapsulate state in streams. Now not everyone is familiar with Scheme, therefore it’s sometimes useful to express things in a language that’s closer to pseudocode: Python.

Let’s align on terminology

First of all, linked lists:

  +---+---+   +---+---+   +---+---+
  | 1 |  -+-->| 2 |  -+-->| 3 |  -+--> None
  +---+---+   +---+---+   +---+---+

A linked list consists of tuples (head, tail). head is the first list element, tail is the remainder of the list. If there is no remainder, tail is a special symbol representing the empty list, often NULL/nil/None.

Iterating through linked lists is easy. Just use the head and tail of each tuple to navigate your way through the list. When encountering nil, stop the iteration. This lends itself well for functional programming.

Delayed linked lists

Delayed linked lists are almost the same, but with a twist: Instead of storing the tail directly, they store a procedure that evaluates to the tail. This may sound silly, but has the interesting application of allowing to model lists of infinite size.

The following implementation in Python also caches the results of each calculation in the linked tuples:

class Stream(object):
  def __init__(self, head, delayed_tail):
    self._head = head
    self._delayed_tail = delayed_tail

  @property
  def head(self):
    return self._head

  @property
  def tail(self):
    if not hasattr(self, "_tail"):
      self._tail = self._delayed_tail()
      del self._delayed_tail
    return self._tail

  # The following two methods are just for easier debugging.
  def take(self, n):
    if n > 0:
      tail = self.tail
      if tail:
        return [self.head] + self.tail.take(n - 1)
      else:
        return [self.head]
    else:
      return []

  def __repr__(self):
    return "[%s...]" % (", ".join(map(repr, self.take(10))))

Examples: Infinite streams of integers

For example, this is the infinite list that contains only ones:

  >>> ones = streams.Stream(1, lambda: ones)
  >>> ones
  [1, 1, 1, 1, 1, 1, 1, 1, 1, 1...]

You can also create helper functions to do componentwise operations:

  >>> streams.add_streams(ones, ones)
  [2, 2, 2, 2, 2, 2, 2, 2, 2, 2...]

“add_streams” is defined like this:

def add_streams(a, b):
  if a and b:
    return Stream(a.head + b.head,
                  lambda: add_streams(a.tail, b.tail))
  else:
    return None

This is a definition of the natural numbers:

>>> N = Stream(0, lambda: add_streams(ones, N))
>>> N
[0, 1, 2, 3, 4, 5, 6, 7, 8, 9...]

Encapsulating state from unknown sources

And finally, you can use this to encapsulate state that comes from an unknown source, like a network socket, into a delayed list of tuples with an immutable interface to users.

The following function creates a stream from a Python generator (or any other stateful Python iterable*). The trick here is that we rely on the lazy stream caching its results, so that we can guarantee the iterator is called exactly once for each stream element.

def stream_from_generator(g):
  try:
    item = g.next()
    return Stream(item, lambda: stream_from_generator(g))
  except StopIteration:
    return None

[*] = A Python iterable is an object that you can call obj.next() on. It will return something else on every call, and eventually raise a StopIteration exception, when it’s out of elements.

Posted by: t_fischer

Recently I purchased an external USB harddrive as a replacement for a failing old one. This device came with NTFS preconfigured, but as I plan to use the drive under Linux, I am looking for alternatives.

Heyho zusammen,

am kommenden Samstag, den 01.06., findet ab 11 Uhr morgens wieder das allmonatliche Fachschaftsaufräumen statt. Fleißige Helfer sind wie immer gerne in Massen gesehen.

Da die Tür Samstags für gewöhnlich abgeschlossen ist, werden alle transponderlosen Helfer gerne unter der Telefonnummer 0631-205-2553 hereingelassen.

Viele Grüße,
Jonathan und Markus

Frage: „omfgomfg Dein dummes Nicht-Windows kann ja nicht mal DVDs abspielen!!11einself“

Antwort: Installiere lubuntu-restricted-extras und libdvdread4. Führe (als root) /usr/share/doc/libdvdread4/install-css.sh aus. Etwa so:

sudo apt-get install lubuntu-restricted-extras libdvdread4
sudo /usr/share/doc/libdvdread4/install-css.sh

Die nächste FSR-Sitzung findet am 29.5. um 15:30 im Sofaraum statt.

Die vorläufige Tagesordnung sieht wie folgt aus:

0 – Festlegen der TO
1 – Mitteilungen
2 – AStA Sommerfest
3 – Änderung von Referaten
4 – Anträge
5 – Protokolle
6 – Verschiedenes

Schickt bitte Tagesordnungsänderungswünsche, schriftliche Berichte zum Protokoll, oder geplante Anträge vorher rum.

Dear blogosphere,

Last week, in my hobby project in C, I fell for the classic bug of
doing an assignment in the conditional of an if
statement. I knew about this for years, and yet I made this
mistake!

  if (expected_arg_count = actual_arg_count) {
    // ...
  }

I should be running a linter. Any recommendations?

Häufig möchte ich eine Datei oder einen Link von einem Gerät auf ein anderen im Heimnetz schicken. Gero hatte vorgeschlagen, die Chrome-Tabs von einem Gerät auf ein anderes zu schicken. Das ist prinzipiell eine recht hübsche Angelegenheit. Diese Möglichkeit setzt jedoch voraus, dass der eigene Chromium-Browser über den Google-Account synchronisiert ist. Außerdem beschränkt sich dieser nette Trick auf den Austausch von Links zu vorhandenen Dokumenten. Wer jedoch private Dateien durch das Heimnetz schicken möchte, kann dies (fast) mit den Bordmitteln einer aktuellen Linuxdistribution tun: Die jede ist vom zerconf/avahi-Chat.

Zunächst sollte Avahi mDNS/DNS-SD daemon installiert sein. Dadurch „finden“ sich die Computer bzw. die darauf laufenden Dienste serverlos im lokalen Netzwerk. Nun fehlt noch ein geeigneter Chat-Client. Unter vielen Linuxdistributionen ist oft sind oft die Chatprogramme Empathy oder Pidgin installiert. Auch der reine XMPP-Client Gajim kann verwendet werden.

Ich habe mich für Pidgin entschieden. Dort musste ich einfach ein neues Chatkonto für das Protokoll „Bonjour“ einrichten. Ich musste mir lediglich einen Namen aussuchen und „Speichern“ klicken. Das ist alles. Unter Empathy hätte ich ein „Personen in der Nähe“-Konto eingerichtet und unter Gajim hätte ich das vorhandene „local“-Konto aktiviert.

Ist das Konto eingerichtet, tauchen die anderen Nutzer im Netzwerk automatisch in der Kontaktliste auf - ganz ohne Registrieren, Anmelden und „Kontakte hinzufügen“. Nun können einfach Dateien oder Textnachrichten wie etwa Links versendet werden.

Seit dem 21. Mai 2013 könnt ihr euch für eure Prüfungen anmelden. In der Regel geschieht dies im QIS.

Ihr habt genau 3 Wochen Zeit, um euch zu entscheiden, was ihr dieses Semester prüfen wollt. Die Frist endete für Erstanmelder im Bachelor am 29. Mai 2013, Erstanmelder im Master haben, ebenso wie alle anderen, noch bis zum 11. Juni 2013 Zeit. Eine vollständig Liste der Fristen und Termine findet ihr hier

Mündliche Prüfungen sind etwas anders geregelt: Diese müssen mindestens zwei Wochen vor dem Prüfungstermin im Prüfungsamt angemeldet werden. Die notwendigen Formulare gibt’s direkt dort, an der Fachschaftspinnwand vor Raum 48-452 und auch online.

Servus liebe Leser!

Seit längerem habe ich mich schon gefragt, ob es eine effiziente Möglichkeit gibt, Webseiten von meinem Laptop/Smartphone/Tablet/Phablet/Whatever auf den Browser meines Heim-PC’s zu senden oder anders herum.

Nun habe ich herausgefunden, das Google Chrome von Haus aus eine sehr komfortable Lösung mitbringt! Voraussetzung ist natürlich, dass man Chrome mit einem Google Account zur Browser-Daten-Synchronisation verwendet.  Chrome ermöglicht es, automatisch die Tabs aller Geräte im Hintergrund mit der Cloud zu synchonisieren (Dazu müsst ihr mit eurem Google Account verbunden sein) und, von jedem beliebigen gerät mit Google Chrome, komfortabel in wenigen Klicks wieder abzurufen. Folgendes muss man tun:

1. (Auf allen Geräten sicherstellen, dass die Tab-Synchronisation mit dem Google Konto eingeschaltet ist. Sollte bei eingeschalteter Synchronisation schon der Fall sein. PC: Menü > Einstellungen > Erweiterte Synchronisierungseinstellungen > Geöffnete Tabs. Android: Menü > Einstellungen > [Euer Accountname] > Synchronisieren > Geöffnete Tabs)
2. Einen neuen Tab öffnen und in der Übersicht für leere Tabs auf Andere Geräte klicken (Auf Smartphones ist es ein Ordner-Icon mit zwei Pfeilen). Es öffnet sich folgendes Menü:
   

   Browser Tabs in Chrome gerät-übergreifend öffnen

3. … in dem ihr dann ganz einfach die Websites eurer anderen Geräte in dem neuen Tab öffnen könnt.

Vielleicht hatte der ein oder andere von euch auch einen Aha!-Moment, ich habe die Funktion lange genug übersehen

Man liest sich!

Mehr Details: https://support.google.com/chrome/answer/2591582?hl=de

Gerade jetzt zur Zeit der Jahrmärkte und Dorffeste treibt eine widerlich-klebrige von Mainstreamkinos bekannte, als Wurfgeschoss missbrauchte Masse ihr Unwesen in Deutschland. Die Rede ist vom so genanten Popcorn. Dem guten Puffmais wird jedoch bei dieser Verallgemeinerung Unrecht getan. Denn dieser existiert jedoch nicht nur in seiner widerlich-klebrigen gezuckerten Variante. Dies scheint offenbar nur eine deutsche Zubereitungsart zu sein. Etwa in den USA ist diese gezuckerte Version eher unbekannt. Dort ist höchstens gelegentlich „Kettle Corn“ vorzufinden. Dieses Knabberwerk wird zwar auch mit Zucker und Öl hergestellt, enthält jedoch dennoch Salz. Somit unterscheidet es sich vom deutschen Zuckerpopcorn, das ja gar nicht salzig ist. Übrigens ist salziges Popcorn in den vereinigten Staaten gar nicht unüblich. Es ist sogar die Regel! Amerikanisches Popcorn ist meist salzig. Das Salz wird meist nach der Zubereitung zugegebn.

Die Variantenvielfalt bei Popcorn ist nicht auf Zucker und Salz beschränkt. Eine eher untypische Variante ist das fein-würzige Popcorn. Es ist zuckerfrei und hat einen leichten Chiligeschmack. Diese Popcornart ist nicht nicht unebdingt jedermanns Geschmack. Es lohnt sich jedoch dies ein mal zu probieren – nicht nur als Testlauf für hausgemachtes Chiliöl.

Hausgemachtes Chiliöl

Eine wichtige Zutat beim würzigen Popcorn ist das Chiliöl. Dieses verleiht Popcorn und vielen anderen Speisen einen leicht-würzigen Geschmack. Chiliöl gibt es im gut sortierten Supermarkt zu kaufen. Allerdings lässt es sich deutlich preiswerter aus handelüblichem Speiseöl und Chiliflocken, also zerkleinerten, getrockneten Chilischoten herstellen.

Zur Herstellung benötigt werden Chiliflocken, Öl, eine Flasche und ein Trichter. Als Öl ist ein natives Olivenöl oder „Natives Olivenöl Extra“ zu empfehlen. Ideal, aber eher selten ist kaltgepresstes Maisöl. Eher abzuraten ist von Sonnenblumenöl.

Zunächst wird eine zwei Finger breite Schicht Chiliflocken mithilfe des Trichters in die Flasche gefüllt. Anschließen wird das Öl dazugegeben. Nun muss die Flasche kräftig durchgeschüttelt werden. Anschließend wird die Flasche in den Kühlschrank gestellt. Die Flocken quellen auf. Das Öl wird dickflüssig. Alle zwei bis drei Tage muss das Öl aus dem Kühlschrank genommen werden. Wenn es warm wird, setzen sich die Flocken langsam auf dem Boden ab. Nun wird das Öl wieder ein mal kräftig durchgeschüttelt und für die nächsten zwei bis drei Tage in den Kühlschrank gestellt.

Mit der Zeit nimmt das Öl eine gesunde rote Farbe an. Nach zwei Wochen kann es dann verwendet werden. Dazu kann das Öl durch ein Sieb umgefüllt werden, um keine Flocken mehr im Endprodukt zu haben. Es ist jedoch auch möglich die Flocken im Öl zu belassen. Bei vorsichtigem Ausgießen gelangen dann auch keine oder kaum Flocken in das Nahrungsmittel.

Würziges Popcorn mit leichtem Chiligeschmack

Das so hergestellte Chiliöl kann nun verwendet werden, um würziges Popcorn herzustellen. Neben dem Öl werden hierzu Puffmais (auch bekannt als Popcornmais, erhältlich im Supermarkt) und eine Pfanne mit durchsichtigem Deckel benötigt. Ist keine Pfanne verfügbar, kann auch ein Topf verwendet werden. Auf den Deckel sollte jedoch auf gar keinen Fall verzichtet werden!!1! (Es sei denn, dies geschieht für eine Fernsehsendung von Wigald Boning und Bernhard Hoëcker)

Zunächst muss die Oberfläche der Pfanne mit etwas Chiliöl benetzt werden. Gerade so viel, dass es reicht, um die Pfanne dünn damit zu bedecken. Es ist darauf zu achten, dass keine Chiliflocken in der Pfanne sind! Diese verbrennen nämlich und hinterlassen einen stechenden, die Schleimhäute reizenden Geruch. Das muss nicht sein. Nun muss das Öl so lange erwärmt werden, bis ein klein wenig Rauch aufsteigt. Dann sollte die Wärme etwas reduziert werden.

Danach werden die Maiskörner zugegeben. Hierbei sind so viele Maiskörner zu verwenden, dass die Hälfte der Pfanne mit einer Schicht der Körner bedeckt ist. Ist die Hälfte bedeckt, wird der Deckel aufgesetzt und die Maiskörner werden durch Rütteln über die ganze Pfanne verteilt.

Sobald die Körner zu knallen anfangen, muss die Pfanne gelegentlich gerütttelt werden. Sobald es nach intensivem Knallen keine entsprechenden Kanllgeräusche mehr gibt, muss die Pfanne von der Feuerstelle genommen werden.

Das deduktive System F₀ ist ein Kalkül. Es erlaubt durch eine reine Betrachtung des „wörtlichen“ (syntaktischen) Aufbaus einer Aussage Folgerungen zu treffen. Dies beutet außerdem, dass automatisiert Beweise für Aussagen gefunden werden können.

Wie jeder Kalkül gibt auch F₀ eine Menge von Axiomen (eigentlich: Axiomschemata) und Regeln vor. F₀ verwendet „Modus Ponens“ als einzige Regel. „Modus Ponens“ besagt, dass die rechte Seite einer Implikation bewiesen ist, wenn schon die Implikation selbst und die linke Seite bewiesen wurden. Gibt es also einen Beweis für A → B und A, so kann auch B als bewiesen angenommen werden. Die Axionsschemata in F₀ sind drei Formen Tautolgien, die nur die Negation (¬) und die Implikation (→) verwenden. Durch Einsetzen beliebiger Formlen (die nur → und ¬ verwenden) in diese Schemata, lassen sich bewiesene Aussagen generieren.

Neben den Axiomen gibt es außerdem noch eine Reihe von Theoremem, die schon bewiesen sind und wie die Axiomschemata verwendet werden dürfen. Auf der Webseite zur Logik im Sommersemester 2011 (Madlener) ist eine Zusammenfassung der Kalküle zu finden. Diese beinhaltet elf Theoreme und die drei Axiome aus F₀

Beispiel: z.Z. ⊢_F0 B → (¬C → ¬(B → C))

Wie wird ein Beweis in F₀ nun aufgeschrieben? Ich werde dies nun vorführen, indem ich Beweise, dass B → (¬C → ¬(B → C)) eine Tautologie ist. Die bedeutet, dass ich nur die Axiome (und nach Belieben die bewiesenen Theoreme) verwenden darf, um die Aussage herzuleiten. Es bietet sich an, das Deduktionstheorem anzuwenden:

• z.Z. ⊢_F0 B → (¬C → ¬(B → C))
• z.Z. B ⊢_F0 ¬C → ¬(B → C)

Es genügt also B als bewiesen anzunehmen und ¬C → ¬(B → C) herzuleiten.

1. B (als bewiesen angenommen)
2. ((B → C) → C) → (¬C → ¬(B → C)) (Theorem 8)
3. B → ((B → C) → C) (Theorem 5)
4. (B → C) → C (Modus Ponens 1. und 3.)
5. ¬C → ¬(B → C) (Modus Ponens 3. und 2.)

Das war es auch schon. Wichtig ist hierbei, immer die verwendeten Axiome (beziehungsweise Theoreme) und die mit Modus Ponens resultierenden Folgerungen getrennt voneinander auszuschreiben. Hier etwa hätte es nicht genügt 4. aufzuschreiben, ohne vorher 3. zu kennzeichnen!

Beispiel: z.Z. ⊢_F0 (A → B) → (¬B → ¬A)

Im vorigen Beispiel wurde das Theorem 8 verwendet. Als weiteres Beispiel werde ich dieses nun herleiten. Es erinnert stark an Axiom 3 ((¬A → ¬B) → (B → A)). Durch Einsetzen von ¬A und ¬B in Axiom 3 lässt sich auch etwa sehr Ähnliches bekommen: (¬¬A → ¬¬B) → (¬B → ¬A) In der semantischen Welt könnte einfach ¬¬A durch A und ¬¬B durch B ersetzt werden. Da in F₀ jedoch alles syntaktisch ist, geht das nicht. Es ist insbesondere auch nicht erlaubt die Negationen wegzulassen und „siehe Theorem 3 (¬¬A → A)“ zu schreiben. Sinnvoll ist hier ein Zwischenbeweis.

Zwischenbeweis: z.Z. ⊢_F0 (A → B) → (¬¬A → ¬¬B)

Zweifache Anwendung des Deduktionstheorems

• z.Z. ⊢_F0 (A → B) → (¬¬A → ¬¬B)
• z.Z. (A → B) ⊢_F0 ¬¬A → ¬¬B
• z.Z. (A → B), ¬¬A ⊢_F0 ¬¬B

(A → B) und ¬¬A werden also als gegeben angenommen und ¬¬B ist herzuleiten.

1. A → B (als bewiesen angenommen)
2. ¬¬A (als bewiesen angenommen)
3. ¬¬A → A (Theorem 3)
4. A (Modus Ponens 2. und 3.)
5. B (Modus Ponens 4. und 1.)
6. B → ¬¬B (Theorem 7)
7. ¬¬B (Modus Ponens 5. und 6.)

Anwendung des Zwischenbeweises

Der Zwischenbeweis ist nun ungemein hilfreich. Zunächst wird das Deduktionstheorem benutzt.

• ⊢_F0 (A → B) → (¬B → ¬A)
• (A → B) ⊢_F0 (¬B → ¬A)

Nun kann der Zwischenbeweis leicht eingesetzt werden:

1. A → B (als bewiesen angenommen)
2. (A → B) → (¬¬A → ¬¬B) (Aus dem Zwischenbeweis)
3. ¬¬A → ¬¬B (Modus Ponens 1. und 2.)
4. (¬¬A → ¬¬B) → (¬B → ¬A) (Axiom 3)
5. ¬B → ¬A (Modus Ponens 3. und 4.)

Weitere Beispiele finden sich in den Übungsaufgaben vom Sommersemester 2011.

Hoiho,

hiermit möchte ich euch ganz herzlich zur nächsten FSR-Sitzung am 15.5. um 15:30 im Sofaraum einladen.

Die vorläufige Tagesordnung sieht wie folgt aus:

0 – Festlegen der TO
1 – Mitteilungen
2 – Emailverteiler
3 – AStA Sommerfest
4 – VLU Ergebnisse letzes Semester
5 – Anträge
6 – Protokolle
7 – Verschiedenes

Kurze Anmerkung zu Punkt 2: Am Freitag um 17 Uhr treffen wir (bisher Schumb und ich, weitere sind gern gesehen) uns in der Fachschaft und überlegen uns ein Konzept für die Emailverteiler und stellen das dann in der Sitzung vor.
Zu Punkt 4: Die Ergebnisse wurden – soweit ich weiß – noch nicht sinnvoll ausgewertet und zumindest gefühlt gibt es da Bedarf, dass wir uns das anschauen sollen. Ich will da nichts Inhaltliches machen, sondern nur das weitere Vorgehen besprechen.

Schickt bitte Tagesordnungsänderungswünsche, Schriftliche Berichte zum Protokoll, oder geplante Anträge vorher rum.

Wer sich mit Informatik oder Mathematik beschäftigt, wird früher oder später einen Beweis führen. Etwa bei der Zugabe zu „Mathematische Folgen“ war das der Fall. Bei endlich vielen Fällen ist das eher überschaubar: Um etwa zu beweisen, dass alle Kinder von Hanspeter größer als 1,40m sind, muss man einfach zu Klaus, Franz und Giesela gehen und nachmessen. Spannend wird es, wenn (wie im genannten Beispiel) über unendlich viele Fälle gesprochen wird.

Im vorliegenden Fall wurde die vollständige Induktion benutzt. Diese bietet sich an, wenn über natürliche Zahlen gesprochen wird, die die Fälle durchnummereien. Zunächst wird eine kleinste natürliche Zahl identifiziert und für den zugehörigen (meist trivialen) Fall ein Beweis geführt. Dies ist der Induktionsanfang. Im Anschluss wird eine Induktionsbehauptung aufgestellt, die besagt, dass es eine Zahl n gibt, bis zu der die zu beweisende Behauptung nachgewiesen ist. Im folgenden Induktionsschritt wird nun gezeigt, dass die Behauptung, so sie denn für n gilt, auch für den Nachfolger gilt. Nun ist die Aussage für jeden beliebige der unendlich vielen Fälle bewiesen, da sich jeder natürliche Zahl (also auch jeder Fall) durch entsprechend häufige Anwendung des Induktionsschrits erreichen lässt.

Induktion ohne natürliche Zahlen

Nun kann es sein, dass unsere Menge von Fällen gar nicht über die natürliche sondern etwa rekursiv definiert ist. Das kann so aussehen:

• Die Menge enthält die Worte „UND“, „NUDELN“ und „POMMES“.
• Für jedes Wort der Menge sind auch die Wörter enthalten, die durch Anhängen von „_UND_NUDELN“ und „_UND_POMMES“ entstehen.
• Die Menge ist genau die von den ersten beiden Punkten beschriebe Menge. (Es sind alle so erzeugbaren Wörter enthalten und sonst nichts)

Wie beweist man nun Behauptungen wie „In jedem Wort kommen ‚NUDELN‘ und ‚POMMES‘ höchstens ein mal öfter als ‚UND’ vor.“? Nun, wir haben zwar keine natürlichen Zahlen zu Verfügung, es lässt sich jedoch ein ähnliches Muster erkennen: Der erste Punkt stellt Anfangselemente dar (entspricht 0 oder 1 bei natürlichen Zahlen), der zweite erläutert, wie die Nachfolger der Elemente rekursiv gebildet werden (entspricht n+1 bei natürlichen Zahlen). Ein Beweis funktioniert dann so:

Beispiel einer strukturellen Induktion

Zu zeigen: anzahl_nudeln(w) ≤ anzahl_und(w) + 1 sowie anzahl_pommes(w) ≤ anzahl_und(w) + 1

Induktionsanfang

Sei w das Wort „UND“, „NUDELN“ oder „POMMES“ aus der Sprache.

• w ≡ „UND“: anzahl_und(w) = 1; anzahl_nudeln(w) = anzahl_pommes(w) = 0. ✓
• w ≡ „NUDELN“: anzahl_und(w) = anzahl_pommes(w) = 0; anzahl_nudeln(w) = 1. ✓
• w ≡ „POMMES“: anzahl_und(w) = anzahl_nudeln(w) = 0; anzahl_pommes(w) = 1. ✓

Induktionsvoraussetzung

Die zu zeigende Behauptung gelte für ein Wort w.

Induktionsschritt

Die Behauptung gilt für das Wort w. Zeige nun, dass sie auch für das Wort w*, das durch Anhängen von „_UND_NUDELN“ oder „_UND_POMMES“ entsteht.

• w* entsteht durch Anhängen von „_UND_NUDELN“. anzahl_und(w*) = anzahl_und(w)+1; anzahl_nudeln(w*) = anzahl_nudeln(w)+1; anzahl_pommes(w*) = anzahl_pommes(w); nach IV: anzahl_pommes(w) ≤ anzahl_und(w) + 1 → anzahl_pommes(w*) ≤ anzahl_und(w) + 1 + 1 → anzahl_pommes(w*) ≤ anzahl_und(w*) + 1; Nach IV: anzahl_nudeln(w) ≤ anzahl_und(w) + 1 → anzahl_nudeln(w) + 1 ≤ anzahl_und(w) + 1 + 1 → anzahl_nudeln(w*) ≤ anzahl_und(w*) + 1 ✓
• w* entsteht durch Anhängen von „_UND_POMMES“: analog.

QED

Nun wurde die Aussage für alle Elemente der unendlichen Menge gezeigt, da die elementaren Wörter der Behauptung genügen und die Bildungsvorschriften die Behauptung erhalten. Gut. Das war quick-and-dirty. Die Wikipedia und das Logikskript (2002, Madlener, S.2) erklären das noch mal richtig. Die verwendete Sprache ist übrigens an ein Beispiel aus „Software-Entwicklung 3“ (Gotzhein) angelehnt.

Jabber ist ein dezentrales Chatsystem auf Basis des freien Standards XMPP. Jabber ermöglicht eine Kontaktliste mit Statusanzeige, Einzelchats, Konferenzen, teilweise auch Audio-/Videoübertragung und vieles mehr. Jeder kann einen eigenen Server aufsetzen oder einen der bestehenden verwenden. Nachrichten, die an Nutzer fremder Server gehen, werden vom eigenen Server an den fremden weitergeschickt.

Viele Nutzer besitzen schon einen Jabber-Account, ohne es zu wissen. E-Mail-Accounts von United Internet (GMX, web.de, 1und1), Google Mail und Yandex sind schon funktionierende Jabber-Accounts. Wer noch keinen Jabber-Account besitzt, kann etwa bei jabber.fsinf.de einen anlegen.

Auch benutzen viele Nutzer Jabber/XMPP-fähige Clients (wie Pidgin), ohne es zu merken. Wer noch einen geeigneten Client sucht, findet eine knappe Auswahl mit Anleitungen bei einfachJabber.de und eine große Liste bei xmpp.org.

Warum ist das gerade jetzt wichtig?

Seit Jahren wird darauf hingewiesen, dass zentralisierte Chatdienste wie ICQ einzelnen Anbietern eine große Macht geben und durchaus gefährlich sind. In erster Linie wurde hierbei auf eine Passage in den Nutzungsbedingungen von ICQ verwiesen, wonach der Betreiber beliebges Material, das an die ICQ-Dienste geschickt wird, beliebig verwenden, verarbeiten, speichern und weitergeben kann (siehe Abschnitt „Materials You Send or Post“ in der ICQ-EULA).

Was ein Betreiber eines zentralisierten Kommunikationsdienstes noch so anstellen kann, demonstriert der ICQ-Eigentümer mail.ru zur Zeit: Die Server filtern Links zu YouTube aus den privaten Chatnachrichten aus.

Liebe Informatikstudenten,

am Mittwoch, 24.4.2013 findet um 13:45 Uhr die nächste Vollversammlung aller Informatikstudierenden in Raum 42-110 statt. Dazu seid ihr alle herzlich eingeladen.

Die vorläufige Tagesordnung sieht so aus:

1. Festlegung der Tagesordnung
2. Rechenschaftsbericht des Fachschaftrats
3. Studienangelegenheiten
4. Anträge (falls vorhanden)
5. Entlastung des Fachschaftrats
6. Neuwahlen des Fachschaftsrats
7. Verschiedenes
8. Ausgabe der Mohrenköpfe

Die konstituierende Sitzung findet diesmal nicht direkt im Anschluss statt, sondern am Freitag, 26.4. um 15:30 in Raum 48-462. Zum Warmklüngeln und Überblick verschaffen, wer sich aufstellen lassen will bzw. wer welche Referate übernehmen will, haben wir ein Etherpad eingerichtet.