An Application of Semantic Web Technology to Mathematical Knowledge Management
Kenny Luck
Table of contents
A bit about myself
The main ideas of this project
Introduction to HOL, some history
Architecture of the codes
Design Issues (i.e. ideas, things to be discussed, etc.)
A Bit About Myself
I'm ...
a senior math major
a fan of science
a big fan of the Semantic Web
..., so I spent quite some time hacking HOL Light, a famous interactive theorem prover
Main Ideas
My opinion: symbol-symbol (URI reference) triples are interesting, symbol-literal triples (e.g. some DBpedia triples) are not.
Good example: relation between a person and a person (foaf:knows)
Our example: the dependency among theorems and proofs in mathematics (a theorem can be proved by this proof, the proof depends on these theorems,...)
This is essecially an RDFizing project. The data is already decentralized. We just make these links explicit.
We are looking for applications based on the RDF represented mathematical knowledge. This should be a good playground for various braches of AI.
By the way, the RDF store we use is cwm
Introduction to HOL light - some history
originates from LCF, a proof checker developed by Robin Milner, a Turing Award Laureate
has only 8 basic inference rules (equality, modus ponens, variable substitution, etc.) exercise for myself: write these rules down with N3 rules
all other rules are just strategies for applying the basic rules
a proof in HOL is roughly a sequence of rules (see also: Design Issue: how to globalized local identifiers)
An Application: Decentralized Publishing/Tracing
Demo - (can we call this backward chain learning?)
the therorems are stored decentrally, linked via RDF
Prove -> Found unkown object -> Fetch -> Prove .....
Fetch decentrally
Design Issue: what should be the answer to a SPARQL ASK?
The next intelligent step should be making deductive databases
ASK {?x a holbasic:Theorem. ?x holbasic:holstring "1+1=2"} should return yes
ASK {?x a holbasic:Theorem. ?x holbasic:holstring "1+1=3"} should return no, because "not 1+1=3" is provable. We assume mathematics is consistent, or...
ASK {?x a holbasic:Theorem. ?x holbasic:holstring "x^n+y^n=z^n/\ n>3 => x=0"} should return unkown and provide useful metadata (how long did the attempt execution take? what were the methods?)
Is there protocol for retriving why "1+1=2"?
Godel Incompleteness Theorem vs. Open World Assumption
Design Issue: how to globalized local identifiers
we want to make holbasic:holstring an Inverse Functional Property so that the same theorems are smushed. This prevents ocassional "mathematician B discovered this theorem independently..."
Difficulties: opearators are overloaded throughout mathematics. The meaning of a plus of two vectors and a plus of two numbers is different.
The Semantic Web way of doing this must have something to do with using URI to identify things.
My Solution: RDFa-like annotation. For example, "u + v" becomes "u <a about="http://example.com/vector#plus">+</a> v"
