Mathematik als Anwendungsfall und Herausforderung für das Semantic Web

Motivation Ansatz Doktorarbeit Fazit

Mathematik als Anwendungsfall undHerausforderung für das Semantic Web

Doktorandenforum Natur+Wissenschaft

Christoph Lange

Jacobs University Bremen

8. Dezember 2008

Ch. Lange (Jacobs University) Mathematik im Semantic Web 8. Dezember 2008 1

http://kwarc.info

http://www.jacobs-university.de



Hello, World!

Christoph Lange, Informatik, Jacobs University BremenFachgebiet: Semantic Web, Mathematical KnowledgeManagement (Verbindung von beidem)Stadium: Bausteine zu Ende führen und in größerenZusammenhang setzenVortragsthema: Überblick über das Forschungsthema


http://kwarc.info



Semiformales mathematisches Wissen

Arbeit mit mathematischem Wissen liegt zwischen den Extremenvöllig unstrukturierter und informaler Text: z. B. Tafelanschriebvollständige Formalisierung: z. B. algebraische Spezifikation

Neue Theorien (Definitionen, Axiome) in Entwicklung, Beweisskizzen,Lehrmaterialien, . . .

ExampleWenn der Dozent weiß, dass eine Beweisskizze korrekt ist, sollte er sieals „Beweis“ klassifizieren und bei einer Suche als solchen findenkönnen.


http://kwarc.info



Kollaboration an mathematischem Wissen

Forschung und Lehre sind kollaborativ:Forschung: Ideen kursieren in der Arbeitsgruppe → Ausarbeitungen

publizieren, Peer-Review” große kollaborativeEntwicklungen

Lehre: Professor, Assistenten und gute Studenten erarbeitenzusammen Übungsaufgaben

Im Computerzeitalter arbeiten wir immer noch mit Bleistift undPapier.Ziel: Integrierte Umgebung zum kollaborativen Bearbeiten, Erkundenund Kommentieren


http://kwarc.info



Ein Wiki für semiformales mathematisches Wissen

Mathematisches Wissen fürs Informationsmanagement zustrukturieren ist harte Arbeit

Lösung: semantisches Markup: Sagen, was Symbole undStrukturen bedeuten – nicht wie sie aussehenDazu muss man denken und Aufwand treiben

Leitgedanke meiner Forschung„Wie können Anwender unterstützt werden, den Aufwand zu treiben,gemeinsam mathematisches Wissen zu strukturieren. Welcheszusätzliche Wissen kann aus ihren Beiträgen erschlossen werden, undwie kann dieses Wissen wiederum genutzt werden, um dieZusammenarbeit zu verbessern?“


http://kwarc.info



Mathematisches (Nicht-)Wissen in Wikis

Fragen, die Wikipedia nichtbeantworten kann (Bsp. Pythagoras):

Suche \sqrt{a^2 + b^2} = coder x^2 + y^2 = z^2Alle Sätze über Dreiecke, für dieein Beweis im Wiki steht„Was bedeutet

√?“


http://kwarc.info



SWiM, ein Semantisches Wiki für Mathematikhttp://swim.kwarc.info, http://wiki.openmath.org


http://kwarc.info


http://swim.kwarc.info

http://wiki.openmath.org


Bausteine und ihr ZusammenhangOpenMath–Wiki andere

SWiM

(Inter)aktiveDokumente

Wissens-repräsentationStrukturenAnnotation

Argumentationermöglicht

abgreifen

FallstudieEvaluation ?

schreibennavigierenabfragen

Diskussionanregen

verstetigenverbessern

Gesprächs-thema

Frontend/BackendIntegration


http://kwarc.info



Forschungsmethode

1 Anwendungszenarien untersuchen, Anforderungenvorhandener Projekte bzgl. Kollaboration sammeln: OpenMathContent Dictionaries, Flyspeck, . . .

2 Durch vorhandene Formalismen gegebeneWissensrepräsentationerweitern/verbessern/anpassen/zurechtstutzen und aufintegrierte Web-Kollaborationsplattform zuschneiden

3 System-Prototypen basierend auf dieser Wissensrepräsentationbauen, ausgewählte Anforderungen aus (1) erfüllen

4 System in diesen Projekten einsetzen, Feedback aus Fallstudiensammeln. GOTO 1.

In Wirklichkeit keine so strikte Trennung ,


http://kwarc.info



Ergebnisse

Strukturen mathematischen Wissens Semantic-Web-gerechtmodelliert. . . und integriert mit Metadaten, rhetorischen Strukturen undArgumentation über math. WissenSemantic-Web-Ontologien auf „mathematischere“ Artmodellieren (expressiver, besser dokumentiert)Kollaborativer Editor (Wiki) für mathematische Dokumente


http://kwarc.info



Fragen

Jedes Teilthema für sich ist nach oben offen; wo denSchlussstrich ziehen?Ergebnisse überprüfen: Machbarkeit bestimmter Vermutungen zuprüfen ist leicht; ob es wirklich Anwender unterstützt oder garmotiviert, ist schwer.Sehr spezielles Anwendungsgebiet:

Vorteil Anwender kennen sich aus, haben sehr genaueWünsche und Vorstellungen

Nachteil Anwender kommen auch ohne mein Systemzurecht, haben überzogene Wünsche („Ich würde jagern, aber. . . “)

Viel Programmieraufwand, hoher Integrationsaufwand: vielEigenleistung, aber auch auf Assistenten angewiesen


http://kwarc.info



Fazit

Web-Kollaboration an semiformalem mathematischem Wissenin einer Umgebung, die das Wissen bearbeiten und

nutzen kannfür Forschung, Entwicklung, Lehremit einem semantischen Wiki

Experimenteller Ansatz: Anforderungen untersuchen, formalesModell entwickeln, in echtem System und echten Anwendungentesten

Web 2.0 für Mathematiker


http://kwarc.info



Das Semantic WebEin herkömmliches Wiki bzw. webbasiertes System versteht dasWissen nicht, das es enthält.

Vision des Semantic Web:Bedeutung von Web-Inhalten für Maschinenverständlich machen (schwache KI)„Internet der Dinge“; Ressourcen mitMetadaten und Beziehungen untereinanderAgenten erschließen Zusammenhänge: z. B.in der Nähe einen guten Arzt finden, der dieKrankheit meiner Mutter behandeln kannund heute offen hat [Berners-Lee et al. 2001]Intelligenter als „Web 2.0“ (aber noch nichtso verbreitet)Theoretischer Hintergrund: Ontologien,Formale Logik, Automatisches Beweisen


http://kwarc.info



Semantische WikisWie „versteht“ ein semantisches Wiki? Wie macht man Wissenexplizit?

normalerweise: 1 Seite =̂ 1 reales KonzeptSeiten und Links haben Typenz. B. „ist Arzt“, „behandelt Krankheit . . . “, „hat Praxis in . . . “Typen definiert in Ontologie, je nach Anwendung mehr oderweniger formalTyphierarchien: „Sokrates ist ein Mensch, alle Menschen sindsterblich, also ist Sokrates sterblich.“

Nutzen: Bessere Navigation, stärkereSuchfunktion, kontextabhängigePräsentation, neue LernmöglichkeitenArbeitsablauf: Schrittweise Formalisierungder Wiki-Seiten mit verteilten RollenBeispiel: Semantic Wikipedia


http://kwarc.info



Math. Knowledge Representation on the SemanticWeb

Knowledge stored in OMDoc, but extracting an RDF outline to makeit operational:

ExampleAn OMDoc document:<omdoc>

<proof id="pyth-proof"for="pythagoras">...

</proof></omdoc>

Extracted RDF graph:

pyth-proof pythagoras

Proof Theoremtype type

proves

proves

<pyth-proof, rdf:type, math:Proof><pyth-proof, math:proves, pythagoras>

Developing ontology based on OMDoc and OpenMath


http://kwarc.info



Ontologies for Mathematical Documents (1)

Previous StateI had a basic ontology that modelled structures ofmathematical knowledge; mainly statements (definition,theorem, proof, examples)

used in SWiM for navigation, queries, internalbookkeeping

Next ChallengeSemi-formal knowledge often comes in documentsthat also contain textThere is a document structure (chapter, section,cross-reference), and a rhetorical structure, bothof which can be independent from themathematical structure.

notDef

sym

fmpfmpfmp exexex

symDefsymDefsymDef

cdcd

contains

cd

renders-Symbol

uses-Symbol

uses-Symbol

contains contains


http://kwarc.info



Annotation

Sections in theeditor

The toolbar

(Implementation by Gordan Ristovski)


http://kwarc.info



Visualisation of Rhetorical Structures

Rhetorical Blocks (SALT)

Rhetorical Relations(SALT, implementing RST)

(Implementation by Jana Giceva)


http://kwarc.info



Visualisation of Rhetorical Structures

Rhetorical Blocks (SALT)

Rhetorical Relations(SALT, implementing RST)

(Implementation by Jana Giceva)Ch. Lange (Jacobs University) Mathematik im Semantic Web 8. Dezember 2008 18

http://kwarc.info



Argumentation about Mathematical KnowledgeItems

Take the survey:tinyurl.com/5qdetd


http://kwarc.info


tinyurl.com/5qdetd


Domain-Specific ArgumentationAssumptions

Possible problems depend on the type of knowledge itemPossible solutions depend on the type of knowledge item and thetype of problemStandard problems have standard solutions, with which softwarecan assist

Survey (tinyurl.com/5qdetd)Common issues: wrong, incomprehensible, uncommon style,underspecified, redundant, truth uncertainCommon solutions: directly improve affected knowledge item,split itWhen issues remain unresolved, it’s mostly due to insufficientrestructuring support


http://kwarc.info


tinyurl.com/5qdetd


Domain-Specific ArgumentationAssumptions

Possible problems depend on the type of knowledge itemPossible solutions depend on the type of knowledge item and thetype of problemStandard problems have standard solutions, with which softwarecan assist

Survey (tinyurl.com/5qdetd)Common issues: wrong, incomprehensible, uncommon style,underspecified, redundant, truth uncertainCommon solutions: directly improve affected knowledge item,split itWhen issues remain unresolved, it’s mostly due to insufficientrestructuring supportCh. Lange (Jacobs University) Mathematik im Semantic Web 8. Dezember 2008 20

http://kwarc.info


tinyurl.com/5qdetd


Domain-Specific Argumentation (Example)

User Interface

discussion page

knowledgeitems

(OMDoc ontology)on wiki pages

theoremforum1

examplepost1: Issue

(Incomprehensible)

post6: Decision

post3: Agree

post2: Idea(ProvideExample)

post4: Disagree

post5: Agree

exemplifies

hasDiscussion(IkeWiki ontology)

has_container

has_replyresponseTo

resolvesInto

positionOn

onIdea

withPositionsonIssue

physical structure(SIOC)

argumentativestructure

RDF Graph


http://kwarc.info


Mathematik als Anwendungsfall und Herausforderung für das Semantic Web

Technology

Transcript of Mathematik als Anwendungsfall und Herausforderung für das Semantic Web