Informatik
Refine
Year of publication
- 2010 (30) (remove)
Document Type
- Working Paper (6)
- Article (5)
- Bachelor Thesis (5)
- Doctoral Thesis (5)
- Book (3)
- Diploma Thesis (2)
- Part of a Book (1)
- Conference Proceeding (1)
- Contribution to a Periodical (1)
- Preprint (1)
Has Fulltext
- yes (30)
Is part of the Bibliography
- no (30)
Keywords
- Formale Semantik (5)
- LHC (3)
- Logik (3)
- Verifikation (3)
- ALICE (2)
- contextual equivalence (2)
- lambda calculus (2)
- letrec (2)
- semantics (2)
- 900 GeV (1)
Institute
- Informatik (30)
- Frankfurt Institute for Advanced Studies (FIAS) (4)
- Präsidium (4)
- Physik (3)
- Medizin (1)
- Psychologie (1)
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. It is designed to perform automatic induction proofs and can also deal with partial functions. This paper provides a reconstruction of the corresponding logic and semantics using the standard treatment of undefinedness which adapts and improves the VeriFun-logic by allowing reasoning on nonterminating expressions and functions. Equality of expressions is defined as contextual equivalence based on observing termination in all closing contexts. The reconstruction shows that several restrictions of the VeriFun framework can easily be removed, by natural generalizations: mutual recursive functions, abstractions in the data values, and formulas with arbitrary quantifier prefix can be formulated. The main results of this paper are: an extended set of deduction rules usable in VeriFun under the adapted semantics is proved to be correct, i.e. they respect the observational equivalence in all extensions of a program. We also show that certain classes of theorems are conservative under extensions, like universally quantified equations. Also other special classes of theorems are analyzed for conservativity.
The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types.
Visualisierung von E-Mail-Traffic mit Schwerpunkt auf eine inhaltliche Analyse von Wortmustern
(2010)
E-Mail hat sich zu einem sehr wichtigen Kommunikationsmittel entwickelt, leidet aber aktuell unter einer massiven Verbreitung unerwünschter und unverlangter Inhalte. Diese können für einen Anwender nicht nur lästig sein, sondern auch die vorhandene Netz- und Speicher-Infrastruktur enorm belasten.
Die Notwendigkeit einer Filterung des E-Mail-Traffic hat zu einer Reihe recht unterschiedlicher Methoden geführt, die computergesteuert eine E-Mail auf ihren Spam-Gehalt untersuchen.
Die Motivation hinter dieser Arbeit ist zu prüfen, ob die besonderen Eigenschaften der visuellen Wahrnehmung eines Menschen als unterstützendes Mittel eingesetzt werden können, um E-Mail-Inhalte zu überprüfen und eventuell vorhandene Wort-Muster, die auf Spam deuten, sichtbar zu machen.
Um dieses Ziel zu erreichen musste zuerst eine geeignete Auswahl spamspezifischer Merkmale getroffen werden. Danach wurden Methoden des Text Minings angewendet, um aus dem Inhalt einer E-Mail strukturierte Daten zu gewinnen, die sich zur Repräsentation einer Nachricht eignen und als Grundlage für eine Visualisierung herangezogen werden können. Basierend auf den vorab ausgewählten Spam-Charakteristika wurdenWorteigenschaften mit Hilfe extern angebundener Wortlisten, regulärer Ausdrücke und unter Einsatz eines Wörterbuches überprüft, und die erhaltenen Ergebnisse flossen neben einer einfachen Gewichtung von Worthäufigkeiten in Form einer anwendungsspezifischen Gewichtung mit ein.
Es wurden anschließend zwei verschiedene Sichten konzipiert, um einem Anwender einen Einblick in die extrahierten Daten zu ermöglichen. Es hat sich herausgestellt, dass besonders Treemaps geeignet sind um die anfallenden Datenmengen kompakt abzubilden, aber gleichzeitig einen notwendigen Detailgrad auf einzelne Worteigenschaften gewährleisten.
Das Konzept wurde prototypisch unter Verwendung des Mailservers Mercury/32 sowie einer MySQL-Datenbank implementiert und konnte teilweise aufzeigen, dass es anhand der von der Engine generierten Strukturen möglich ist, spamspezifische Merkmale einer E-Mail unter Verwendung der gewählten Visualisierungstechniken auf eine Weise sichtbar zu machen, die einem Anwender eine Mustererkennung erlauben.
Die Diplomarbeit wurde als Gemeinschaftsarbeit angefertigt und konnte sinnvoll in zwei Bereiche aufgeteilt werden: Die Engine und die Visualisierung. Die konzeptuellen Überlegungen für das Thema sind größtenteils gemeinsam erfolgt, jedoch liegt der Schwerpunkt von Pouneh Khayat Pour im Bereich der Analyse und der von Yvonne Neidert in der Visualisierung.
Integer point sets minimizing average pairwise L1 distance: What is the optimal shape of a town?
(2010)
An n-town, n[is an element of]N , is a group of n buildings, each occupying a distinct position on a 2-dimensional integer grid. If we measure the distance between two buildings along the axis-parallel street grid, then an n-town has optimal shape if the sum of all pairwise Manhattan distances is minimized. This problem has been studied for cities, i.e., the limiting case of very large n. For cities, it is known that the optimal shape can be described by a differential equation, for which no closed-form solution is known. We show that optimal n-towns can be computed in O(n[superscript 7.5]) time. This is also practically useful, as it allows us to compute optimal solutions up to n=80.
The well-known proof of termination of reduction in simply typed calculi is adapted to a monomorphically typed lambda-calculus with case and constructors and recursive data types. The proof differs at several places from the standard proof. Perhaps it is useful and can be extended also to more complex calculi.
In dyadic communication, both interlocutors adapt to each other linguistically, that is, they align interpersonally. In this article, we develop a framework for modeling interpersonal alignment in terms of the structural similarity of the interlocutors’ dialog lexica. This is done by means of so-called two-layer time-aligned network series, that is, a time-adjusted graph model. The graph model is partitioned into two layers, so that the interlocutors’ lexica are captured as subgraphs of an encompassing dialog graph. Each constituent network of the series is updated utterance-wise. Thus, both the inherent bipartition of dyadic conversations and their gradual development are modeled. The notion of alignment is then operationalized within a quantitative model of structure formation based on the mutual information of the subgraphs that represent the interlocutor’s dialog lexica. By adapting and further developing several models of complex network theory, we show that dialog lexica evolve as a novel class of graphs that have not been considered before in the area of complex (linguistic) networks. Additionally, we show that our framework allows for classifying dialogs according to their alignment status. To the best of our knowledge, this is the first approach to measuring alignment in communication that explores the similarities of graph-like cognitive representations. Keywords: alignment in communication; structural coupling; linguistic networks; graph distance measures; mutual information of graphs; quantitative network analysis