Your personal computer experts

Who we are...

   Who we are

   Our references

   Price list

If you would like to meet with us personally to discuss your needs, please give us a call!

Kraan and Richards
Entfelderstrasse 7
5012 Schönenwerd

Tel 062/849 9746
Fax 062/849 9743

Ina Kraan: Lebenslauf

Ausbildung

Dolmetscherschule Zürich (September 1980 bis Juli 1984)
     1983 Übersetzerdiplom Deutsch, English, Französisch, Niederländisch
     1984 Konferenzdolmetscherdiplom Deutsch, English, Französisch, Niederländisch

Lic. oec. publ., Richtung Wirtschaftsinformatik (Oktober 1985 bis Juli 1990)
     Wirtschaftswissenschaftliche Fakultät, Universität Zürich

PhD in Künstlicher Intelligenz (August 1990 bis Juli 1994)
     Department of Computer Science, University of Texas at Austin, USA (August 1990 bis Dezember 1990)
     MCI fellowship
     Department of Artificial Intelligence, University of Edinburgh, Scotland, UK (März 1991 bis Juli 1994)
     Stipendium der Sandoz AG (1991 und 1992)
     Nationalfonds-Stipendium für angehende Forscher (1993)
     Dissertation: Proof Planning for Logic Program Synthesis
     Betreuung: Prof. Dr. Alan Bundy

Berufliche Erfahrung

Dolmetscherschule Basel (1984 bis 1986). Als Dozentin unterrichtete ich Übersetzung Deutsch-Englisch, Textanalyse und amerikanische und englische Literatur.

Freiberufliche Tätigkeit (1984 bis 1990). Ich arbeitete als freischaffende Übersetzerin und Konferenzdolmetscherin, u.a. für den Springer Verlag (Heidelberg, Deutschland) und für die Kommission der Europäischen Gemeinschaft (Brüssel, Belgien)..

Institut für Informatik der Universität Zürich (1994 bis 1997). Als wissenschaftliche Mitarbeiterin arbeitete ich am Nationalfondsprojekt TokiZ—A toolkit for Z (Oktober 1993 bis Oktober 1995) beziehungsweise dem Folgeprojekt TokiZ II—A proof tool for Z (Oktober 1995 bis Oktober 1997). Bei TokiZ II war ich Mitgesuchstellerin. Beim TokiZ-Projekt geht es um das Design und die Entwicklung von Tools, die die Anwendung formaler Methoden in der Softwareentwicklung unterstützen. Ich entwickelte im Rahmen des TokiZ-Projekts mit Hilfe des generischen Theorembeweisers Isabelle ein Prototyp eines interaktiven Beweissystems für die formale Spezifikationssprache Z. Im Folgeprojekt TokiZ II Projekt geht es um die Entwicklung eines Tools, das die Anwendung formaler Methoden unterstützt, in dem sie automatisiert wird. Das zu entwickelnde Tool ist eine Weiterentwicklung des Prototyps aus dem TokiZ-Projekt..

Kraan and Richards (1994 bis heute). Mitinhaber. Diese Firma ist auf zwei sehr unterschiedlichen Gebieten tätig. Die erste Aktivität ist der Import und Vertrieb schottischer Produkte, insbesondere Scotch Whisky. Während der Entwicklung dieser Firma wurden die Geschäftsprozesse weitgehendst automatisiert, um die Arbeitszeit zu minimieren. Aus dieser Erfahrung wächst die zweite Aktivität der Firma: Wir beraten Kleinfirmen, die Informatik für ihre Geschäftsziele einsetzen wollen, entwerfen ihre Webauftritte, und entwickeln massgescheiderte Back-Office Softwarelösungen.

Die fünf wichtigsten Publikationen

I. Kraan, D. Basin, and A. Bundy, “Middle-out reasoning for synthesis and induction”, Special Issue on Automated Mathematical Induction, Journal of Automated Reasoning, Volume 16, Nos. 1—2, March 1996. Dieser Artikel fasst die wesentlichen Ergebnisse meiner Dissertation zusammen. Es wird gezeigt, wie Metavariablen im automatischen Theorembeweisen dazu verwendet werden können, geeignete Induktionsschemen zu finden und logische Programme zu synthetisieren.

I. Kraan and P. Baumann, “Logical frameworks as a basis for verification tools: A case study”, Proceedings of the Tenth Knowledge-Based Software Engineering Conference (KBSE-95), 1995. An einem Fallbeispiel wird gezeigt, welche Vor- und Nachteile Verifikationswerkzeuge bringen, die in generischen Theorembeweisern implementiert werden.

B. L. Richards, I. Kraan, A. Smaill, and G. A. Wiggins, “Mollusc: a general proof development shell for sequent-based logics”, Proceedings of the Twelfth Conference on Automated Deduction (CADE-94), 1994. Mollusc ist ein Beweisentwicklungs-System. Mit Mollusc ist es möglich, interaktiv oder auch automatisch, mittels einer Taktiksprache und einem Taktikinterpreter, Beweise in benutzer-definierten Logikkalkülen zu konstruieren und zu editieren.

I. Kraan, D. Basin, and A. Bundy, “Middle-out reasoning for logic program synthesis”, Proceedings of the Tenth International Conference on Logic Programming (ICLP-93), 1993. Dieser Artikel zeigt, wie man das Planen von Verifikationsbeweisen logischer Programme für die automatische Synthese logischer Programmen verwenden kann.

B. L. Richards, I. Kraan, and B. J. Kuipers, “Automatic abduction of qualitative models”, Proceed-ings of the Tenth National Conference on Artificial Intelligence (AAAI-92), 1992. Dieser Artikel beschreibt eine implementierte Methode, wie aus Beobachtungen des Verhaltens eines unbekannten Systems ein beweisbar richtiges Modell des Systems automatisch konstruiert werden kann.