MMLKG: Knowledge Graph for Mathematical Definitions, Statements and Proofs

Project

Nowadays, Knowledge Graphs are important and developing in different areas. However, there is a lack of genuinely interoperable datasets representing mathematics that allow for information exchange between datasets in the Web ecosystem.

We address this matter based on the Mizar Mathematical Library, an essential resource for mathematics fully verified by Mizar software. MML includes definitions and theorems with proofs to which authors can easily refer from newly written Mizar articles.

Read the paper

Example Queries

Explore the Mizar Mathematical Library Knowledge Graph using the publicly available MMLKG Neo4j Browser endpoint. For more Cypher queries examples, refer to our paper.

What are the direct super-structures of the structure ZeroStr?

MATCH (n:`Structure-Pattern`)-[:BROADER]->(o:`Structure-Pattern`)
WHERE n.spelling = 'ZeroStr'
RETURN n.absolutepatternMMLId, o.spelling, o.absolutepatternMMLId

Which adjectives are mostly used as negated ones?

MATCH (n:Attribute)
WHERE n.nonocc IS NOT NULL
WITH n.absolutepatternMMLId AS attribute, n.spelling AS spelling, 
  COUNT(n) AS occurrences
RETURN attribute, spelling, occurrences

Which redefinitions of the equality (=) exist?

MATCH (p:`Predicate-Pattern`)-[:MEMBER]->(d:`Predicate-Definition`)
  <-[:MEMBER]-(r:Redefine)
WHERE r.occurs = "true" AND p.spelling = "="
RETURN p.absolutepatternMMLId AS redefinition

What are all the usages of the theorem labeled JORDAN:21?

MATCH (r:`Theorem-Reference`)-[:MEMBER*]->(t:`Theorem-Item`)
WHERE r.MMLId = "JORDAN:21"
RETURN t.MMLId AS theoremID

Identify all adjectives that are most frequently used in a negated form, where the total occurrences do not exceed 10.

MATCH (n:Attribute)
WHERE n.nonocc IS NOT NULL
WITH n.absolutepatternMMLId AS attribute, n.spelling AS spelling,
  COUNT(n) AS occurrences
WHERE occurrences <= 10
RETURN attribute, spelling, occurrences

Return up to 15 adjectives assigned to the adjective empty when applied to the type set.

MATCH (a:`Text-Proper`)<-[:MEMBER*]-(r:`Conditional-Registration`)
  <-[:MEMBER]-(c1:`Adjective-Cluster`)<-[:MEMBER]-(a1:Attribute),
  (r:`Conditional-Registration`)<-[:MEMBER]-(c2:`Adjective-Cluster`)
  <-[:MEMBER]-(a2:Attribute),
  (r:`Conditional-Registration`)<-[:MEMBER]-(t:`Standard-Type`)
WHERE c1.role = "antecedent" AND c2.role = "consequent"
  AND a1.spelling = "empty"
  AND a1.nonocc IS NULL AND t.spelling = "set"
RETURN a2.spelling AS spelling
LIMIT 15

Explore MMLKG in Neo4j Browser

Authentication type: No authentication

Tools

mizgra

Generating a property graph serialization

csvrelgen

Creating complex relationships

metadata_gen

Generating a property graph metadata

esx_verify

Checking semantics correctness

Data

MMLKG Dataset

Mizar Mathematical Library Knowledge Graph

Ready-to-use dataset generated by mizgra. The archive also includes files used to create the dataset, including CSV relation files produced by csvrelgen, metadata with statistics made through the metadata_gen tool, and XSD schema files.

ESX Files Repository

esx_files

Contains mml.lar and ESX files with Mizar mathematical data. Our tools need these files to prepare CSV relation files, full metadata with stats, and our Mizar Mathematical Library Knowledge Graph. The repository also contains XSD schema files for the ESX files.

About Us

Dominik Tomaszuk, PhD

Faculty of Computer Science
University of Bialystok

Semantic Web, Linked Data, Graph Databases, Knowledge Representation

Łukasz Szeremeta, MS

Faculty of Computer Science
University of Bialystok

Property Graphs, Cheminformatics, Semantic Web, Graph Databases, Knowledge Representation

Artur Korniłowicz, DSc

Faculty of Computer Science
University of Bialystok

Formalization of Mathematics, Theorem Proving, Proof Assistants