From e14f509b0c3c51dc3b6ebf5e157542c36ab69fa9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andreas=20Sch=C3=A4rtl?= <andreas@schaertl.me>
Date: Tue, 26 May 2020 13:00:46 +0200
Subject: [PATCH] uloapi: use full ULO.java
This will be very useful for further integration w/ JVM tech.
---
.../java/info/mathhub/uloapi/query/Query.java | 4 +-
.../java/info/mathhub/uloapi/query/ULO.java | 725 +++++++++++++++++-
2 files changed, 705 insertions(+), 24 deletions(-)
diff --git a/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/Query.java b/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/Query.java
index 7467424..21c8441 100644
--- a/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/Query.java
+++ b/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/Query.java
@@ -67,14 +67,14 @@ public class Query {
}
/**
- * Return a list of triplets that define some kind of {@link ULO#INDUCTIVE_ON} relationship.
+ * Return a list of triplets that define some kind of {@link ULO#inductive_on} relationship.
*
* @return The triplets. Limited to a small number, the actual number of matching triplets in the
* underlying RDF4j repository might be way bigger.
*/
public List<Statement> getInductiveStatements() {
final GraphDB.Operation<List<Statement>> operation = (manager, repository, connection) -> {
- final RepositoryResult<Statement> result = connection.getStatements(null, ULO.INDUCTIVE_ON, null);
+ final RepositoryResult<Statement> result = connection.getStatements(null, ULO.inductive_on, null);
final Iterator<Statement> iterator = result.iterator();
final List<Statement> statements = new ArrayList<>();
diff --git a/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/ULO.java b/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/ULO.java
index fc1b050..ef100f4 100644
--- a/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/ULO.java
+++ b/experimental/uloapi/src/main/java/info/mathhub/uloapi/query/ULO.java
@@ -1,38 +1,719 @@
package info.mathhub.uloapi.query;
import org.eclipse.rdf4j.model.IRI;
-import org.eclipse.rdf4j.model.Namespace;
import org.eclipse.rdf4j.model.ValueFactory;
-import org.eclipse.rdf4j.model.impl.SimpleNamespace;
import org.eclipse.rdf4j.model.impl.SimpleValueFactory;
/**
- * Constants for use with ULO, the Upper Library Ontology [1].
+ * Namespace ULO
+ * Prefix: {@code <https://mathhub.info/ulo>}
*
- * [1] https://gl.mathhub.info/ulo/ulo/-/tree/master/
*/
public class ULO {
- private ULO() {}
- /**
- * The ULO namespace: https://mathhub.info/ulo
- */
- public static final String NAMESPACE = "https://mathhub.info/ulo";
+ /**
+ * {@code <https://mathhub.info/ulo>}
+ */
+ public static final String NAMESPACE = "https://mathhub.info/ulo";
- /**
- * The recommended prefix for the ULO namespace: "ulo"
- */
- public static final String PREFIX = "ulo";
+ /**
+ * {@code <https://mathhub.info/ulo>}
+ */
+ public static final IRI NAMESPACE_IRI;
- /**
- * An immutable {@link Namespace} constant that represents the ULO namespace.
- */
- public static final Namespace NS = new SimpleNamespace(PREFIX, NAMESPACE);
+ /**
+ * {@code <ULO>}
+ */
+ public static final String PREFIX = "ULO";
- public final static IRI INDUCTIVE_ON;
+ /**********************
+ * IRI String Constants
+ **********************/
- static {
- final ValueFactory factory = SimpleValueFactory.getInstance();
- INDUCTIVE_ON = factory.createIRI(ULO.NAMESPACE, "inductive-on");
- }
+ /*****************************
+ * Local Name String Constants
+ *****************************/
+
+ /***************
+ * IRI Constants
+ ***************/
+
+ /**
+ * {@code https://mathhub.info/ulo#action-times}
+ * @see <a href="https://mathhub.info/ulo#action-times">#action-times</a>
+ */
+ public static final IRI action_times;
+
+ /**
+ * {@code https://mathhub.info/ulo#aligned-with}
+ * @see <a href="https://mathhub.info/ulo#aligned-with">#aligned-with</a>
+ */
+ public static final IRI aligned_with;
+
+ /**
+ * {@code https://mathhub.info/ulo#alternative-for}
+ * @see <a href="https://mathhub.info/ulo#alternative-for">#alternative-for</a>
+ */
+ public static final IRI alternative_for;
+
+ /**
+ * {@code https://mathhub.info/ulo#antonym}
+ * @see <a href="https://mathhub.info/ulo#antonym">#antonym</a>
+ */
+ public static final IRI antonym;
+
+ /**
+ * {@code https://mathhub.info/ulo#automatically-proved}
+ * <p>
+ * S is automatically proven by a theorem prover, O is an explanatory
+ * string.
+ * @see <a href="https://mathhub.info/ulo#automatically-proved">#automatically-proved</a>
+ */
+ public static final IRI automatically_proved;
+
+ /**
+ * {@code https://mathhub.info/ulo#axiom}
+ * <p>
+ * Logically (using the Curry-Howard isomorphism), an axiom is a
+ * primitive statement, i.e. a declaration without a definiens.
+ * @see <a href="https://mathhub.info/ulo#axiom">#axiom</a>
+ */
+ public static final IRI axiom;
+
+ /**
+ * {@code https://mathhub.info/ulo#check-time}
+ * <p>
+ * time (a natural number giving a time in milliseconds) it took to check
+ * the declaration that introduced the subject
+ * @see <a href="https://mathhub.info/ulo#check-time">#check-time</a>
+ */
+ public static final IRI check_time;
+
+ /**
+ * {@code https://mathhub.info/ulo#constructs}
+ * <p>
+ * S is a constructor for an inductive type or predicate O
+ * @see <a href="https://mathhub.info/ulo#constructs">#constructs</a>
+ */
+ public static final IRI constructs;
+
+ /**
+ * {@code https://mathhub.info/ulo#contains}
+ * @see <a href="https://mathhub.info/ulo#contains">#contains</a>
+ */
+ public static final IRI contains;
+
+ /**
+ * {@code https://mathhub.info/ulo#counter-example-for}
+ * @see <a href="https://mathhub.info/ulo#counter-example-for">#counter-example-for</a>
+ */
+ public static final IRI counter_example_for;
+
+ /**
+ * {@code https://mathhub.info/ulo#crossrefs}
+ * @see <a href="https://mathhub.info/ulo#crossrefs">#crossrefs</a>
+ */
+ public static final IRI crossrefs;
+
+ /**
+ * {@code https://mathhub.info/ulo#declaration}
+ * <p>
+ * Declarations are named objects, they can also have a type and a
+ * definiens.
+ * @see <a href="https://mathhub.info/ulo#declaration">#declaration</a>
+ */
+ public static final IRI declaration;
+
+ /**
+ * {@code https://mathhub.info/ulo#defines}
+ * <p>
+ * A definition defines various objects.
+ * @see <a href="https://mathhub.info/ulo#defines">#defines</a>
+ */
+ public static final IRI defines;
+
+ /**
+ * {@code https://mathhub.info/ulo#definition}
+ * <p>
+ * A logical paragraph that defines a new concept.
+ * @see <a href="https://mathhub.info/ulo#definition">#definition</a>
+ */
+ public static final IRI definition;
+
+ /**
+ * {@code https://mathhub.info/ulo#deprecated}
+ * <p>
+ * S is deprecated (do not use any longer), O is an explanatory string.
+ * @see <a href="https://mathhub.info/ulo#deprecated">#deprecated</a>
+ */
+ public static final IRI deprecated;
+
+ /**
+ * {@code https://mathhub.info/ulo#derived}
+ * <p>
+ * This knowledge item has a definition in terms of (more) primitive
+ * items.
+ * @see <a href="https://mathhub.info/ulo#derived">#derived</a>
+ */
+ public static final IRI derived;
+
+ /**
+ * {@code https://mathhub.info/ulo#docref}
+ * <p>
+ * A URI reference to a place where this knowledge item is documented
+ * (usually in some read-only rich text format).
+ * @see <a href="https://mathhub.info/ulo#docref">#docref</a>
+ */
+ public static final IRI docref;
+
+ /**
+ * {@code https://mathhub.info/ulo#example}
+ * <p>
+ * A logical paragraph that introduces a mathematical example.
+ * @see <a href="https://mathhub.info/ulo#example">#example</a>
+ */
+ public static final IRI example;
+
+ /**
+ * {@code https://mathhub.info/ulo#example-for}
+ * @see <a href="https://mathhub.info/ulo#example-for">#example-for</a>
+ */
+ public static final IRI example_for;
+
+ /**
+ * {@code https://mathhub.info/ulo#experimental}
+ * @see <a href="https://mathhub.info/ulo#experimental">#experimental</a>
+ */
+ public static final IRI experimental;
+
+ /**
+ * {@code https://mathhub.info/ulo#external-size}
+ * <p>
+ * The number of characters (not
+counting whitespace or comments) in the
+ * source code of the subject. This number can be approximate.
+ * @see <a href="https://mathhub.info/ulo#external-size">#external-size</a>
+ */
+ public static final IRI external_size;
+
+ /**
+ * {@code https://mathhub.info/ulo#file}
+ * <p>
+ * A document in a file system.
+ * @see <a href="https://mathhub.info/ulo#file">#file</a>
+ */
+ public static final IRI file;
+
+ /**
+ * {@code https://mathhub.info/ulo#folder}
+ * <p>
+ * A grouping of files and other folders, i.e. above the document level.
+ * @see <a href="https://mathhub.info/ulo#folder">#folder</a>
+ */
+ public static final IRI folder;
+
+ /**
+ * {@code https://mathhub.info/ulo#formalizes}
+ * @see <a href="https://mathhub.info/ulo#formalizes">#formalizes</a>
+ */
+ public static final IRI formalizes;
+
+ /**
+ * {@code https://mathhub.info/ulo#function}
+ * <p>
+ * functions that construct objects, possibly from other objects, for
+ * example in first-order logic the successor fuction.
+ * @see <a href="https://mathhub.info/ulo#function">#function</a>
+ */
+ public static final IRI function;
+
+ /**
+ * {@code https://mathhub.info/ulo#generated-by}
+ * @see <a href="https://mathhub.info/ulo#generated-by">#generated-by</a>
+ */
+ public static final IRI generated_by;
+
+ /**
+ * {@code https://mathhub.info/ulo#hypernym}
+ * @see <a href="https://mathhub.info/ulo#hypernym">#hypernym</a>
+ */
+ public static final IRI hypernym;
+
+ /**
+ * {@code https://mathhub.info/ulo#hyponym}
+ * @see <a href="https://mathhub.info/ulo#hyponym">#hyponym</a>
+ */
+ public static final IRI hyponym;
+
+ /**
+ * {@code https://mathhub.info/ulo#implementation-uses}
+ * @see <a href="https://mathhub.info/ulo#implementation-uses">#implementation-uses</a>
+ */
+ public static final IRI implementation_uses;
+
+ /**
+ * {@code https://mathhub.info/ulo#implementation-uses-implementation-of}
+ * @see <a href="https://mathhub.info/ulo#implementation-uses-implementation-of">#implementation-uses-implementation-of</a>
+ */
+ public static final IRI implementation_uses_implementation_of;
+
+ /**
+ * {@code https://mathhub.info/ulo#implementation-uses-interface-of}
+ * @see <a href="https://mathhub.info/ulo#implementation-uses-interface-of">#implementation-uses-interface-of</a>
+ */
+ public static final IRI implementation_uses_interface_of;
+
+ /**
+ * {@code https://mathhub.info/ulo#important}
+ * <p>
+ * S is important (to someone); O is an explanatory string.
+ * @see <a href="https://mathhub.info/ulo#important">#important</a>
+ */
+ public static final IRI important;
+
+ /**
+ * {@code https://mathhub.info/ulo#inductive-on}
+ * @see <a href="https://mathhub.info/ulo#inductive-on">#inductive-on</a>
+ */
+ public static final IRI inductive_on;
+
+ /**
+ * {@code https://mathhub.info/ulo#inspired-by}
+ * @see <a href="https://mathhub.info/ulo#inspired-by">#inspired-by</a>
+ */
+ public static final IRI inspired_by;
+
+ /**
+ * {@code https://mathhub.info/ulo#instance-of}
+ * <p>
+ * S is and instance of O, iff it is a model of O, inherits from O,
+ * interprets O,
+etc.
+ * @see <a href="https://mathhub.info/ulo#instance-of">#instance-of</a>
+ */
+ public static final IRI instance_of;
+
+ /**
+ * {@code https://mathhub.info/ulo#inter-statement}
+ * @see <a href="https://mathhub.info/ulo#inter-statement">#inter-statement</a>
+ */
+ public static final IRI inter_statement;
+
+ /**
+ * {@code https://mathhub.info/ulo#interface-uses}
+ * @see <a href="https://mathhub.info/ulo#interface-uses">#interface-uses</a>
+ */
+ public static final IRI interface_uses;
+
+ /**
+ * {@code https://mathhub.info/ulo#interface-uses-implementation-of}
+ * @see <a href="https://mathhub.info/ulo#interface-uses-implementation-of">#interface-uses-implementation-of</a>
+ */
+ public static final IRI interface_uses_implementation_of;
+
+ /**
+ * {@code https://mathhub.info/ulo#interface-uses-interface-of}
+ * @see <a href="https://mathhub.info/ulo#interface-uses-interface-of">#interface-uses-interface-of</a>
+ */
+ public static final IRI interface_uses_interface_of;
+
+ /**
+ * {@code https://mathhub.info/ulo#internal-size}
+ * <p>
+ * the number of bytes in the internal representation of the subject
+ * including any inferred objects and generated proofs. This number can
+ * be approximate.
+ * @see <a href="https://mathhub.info/ulo#internal-size">#internal-size</a>
+ */
+ public static final IRI internal_size;
+
+ /**
+ * {@code https://mathhub.info/ulo#justifies}
+ * <p>
+ * A proof can justify a theorem or a definition
+ * @see <a href="https://mathhub.info/ulo#justifies">#justifies</a>
+ */
+ public static final IRI justifies;
+
+ /**
+ * {@code https://mathhub.info/ulo#last-checked-at}
+ * <p>
+ * the time stamp of when the subject was last checked.
+ * @see <a href="https://mathhub.info/ulo#last-checked-at">#last-checked-at</a>
+ */
+ public static final IRI last_checked_at;
+
+ /**
+ * {@code https://mathhub.info/ulo#library}
+ * <p>
+ * A grouping of mathematical documents. Usually in the form of a
+ * repository.
+ * @see <a href="https://mathhub.info/ulo#library">#library</a>
+ */
+ public static final IRI library;
+
+ /**
+ * {@code https://mathhub.info/ulo#library-group}
+ * <p>
+ * A group of libraries, usually on a repository server like GitHub.
+ * @see <a href="https://mathhub.info/ulo#library-group">#library-group</a>
+ */
+ public static final IRI library_group;
+
+ /**
+ * {@code https://mathhub.info/ulo#logical}
+ * <p>
+ * A logical classification of mathematical knowledge items.
+ * @see <a href="https://mathhub.info/ulo#logical">#logical</a>
+ */
+ public static final IRI logical;
+
+ /**
+ * {@code https://mathhub.info/ulo#mutual-block}
+ * <p>
+ * A theory where the delcarations may mutually refer to each other;
+ * examples include mutually recursive functions and types.
+ * @see <a href="https://mathhub.info/ulo#mutual-block">#mutual-block</a>
+ */
+ public static final IRI mutual_block;
+
+ /**
+ * {@code https://mathhub.info/ulo#name}
+ * <p>
+ * the name of a knowledge item give by the user.
+ * @see <a href="https://mathhub.info/ulo#name">#name</a>
+ */
+ public static final IRI name;
+
+ /**
+ * {@code https://mathhub.info/ulo#nyms}
+ * @see <a href="https://mathhub.info/ulo#nyms">#nyms</a>
+ */
+ public static final IRI nyms;
+
+ /**
+ * {@code https://mathhub.info/ulo#organizational}
+ * @see <a href="https://mathhub.info/ulo#organizational">#organizational</a>
+ */
+ public static final IRI organizational;
+
+ /**
+ * {@code https://mathhub.info/ulo#para}
+ * <p>
+ * A logical paragraph with mathematical meaning.
+ * @see <a href="https://mathhub.info/ulo#para">#para</a>
+ */
+ public static final IRI para;
+
+ /**
+ * {@code https://mathhub.info/ulo#paratype}
+ * @see <a href="https://mathhub.info/ulo#paratype">#paratype</a>
+ */
+ public static final IRI paratype;
+
+ /**
+ * {@code https://mathhub.info/ulo#phrase}
+ * <p>
+ * Phrasal structures in mathematical text and formulae, these include
+ * symbols, declarations, and quantifications.
+ * @see <a href="https://mathhub.info/ulo#phrase">#phrase</a>
+ */
+ public static final IRI phrase;
+
+ /**
+ * {@code https://mathhub.info/ulo#physical}
+ * <p>
+ * An organizational unit for the physical organization of mathematical
+ * knowledge into documents or document collections.
+ * @see <a href="https://mathhub.info/ulo#physical">#physical</a>
+ */
+ public static final IRI physical;
+
+ /**
+ * {@code https://mathhub.info/ulo#predicate}
+ * <p>
+ * A predicate is a mathematial object that evaluates to true/false when
+ * applied to enough arguments.
+ * @see <a href="https://mathhub.info/ulo#predicate">#predicate</a>
+ */
+ public static final IRI predicate;
+
+ /**
+ * {@code https://mathhub.info/ulo#primitive}
+ * <p>
+ * This knowledge item does not have a definition in terms of (more)
+ * primitive items.
+ * @see <a href="https://mathhub.info/ulo#primitive">#primitive</a>
+ */
+ public static final IRI primitive;
+
+ /**
+ * {@code https://mathhub.info/ulo#proof}
+ * <p>
+ * A logical paragraph that serves as a justification of a proposition.
+ * @see <a href="https://mathhub.info/ulo#proof">#proof</a>
+ */
+ public static final IRI proof;
+
+ /**
+ * {@code https://mathhub.info/ulo#proposition}
+ * <p>
+ * A statement of a property of a mathematical object or some relation
+ * between some.
+ * @see <a href="https://mathhub.info/ulo#proposition">#proposition</a>
+ */
+ public static final IRI proposition;
+
+ /**
+ * {@code https://mathhub.info/ulo#revision}
+ * @see <a href="https://mathhub.info/ulo#revision">#revision</a>
+ */
+ public static final IRI revision;
+
+ /**
+ * {@code https://mathhub.info/ulo#rule}
+ * <p>
+ * Ruless are statements that can be used for computation, e.g. theorems
+ * that can be used for simplification.
+ * @see <a href="https://mathhub.info/ulo#rule">#rule</a>
+ */
+ public static final IRI rule;
+
+ /**
+ * {@code https://mathhub.info/ulo#same-as}
+ * @see <a href="https://mathhub.info/ulo#same-as">#same-as</a>
+ */
+ public static final IRI same_as;
+
+ /**
+ * {@code https://mathhub.info/ulo#section}
+ * <p>
+ * A physical grouping inside a document. These can be nested.
+ * @see <a href="https://mathhub.info/ulo#section">#section</a>
+ */
+ public static final IRI section;
+
+ /**
+ * {@code https://mathhub.info/ulo#see-also}
+ * @see <a href="https://mathhub.info/ulo#see-also">#see-also</a>
+ */
+ public static final IRI see_also;
+
+ /**
+ * {@code https://mathhub.info/ulo#similar-to}
+ * @see <a href="https://mathhub.info/ulo#similar-to">#similar-to</a>
+ */
+ public static final IRI similar_to;
+
+ /**
+ * {@code https://mathhub.info/ulo#size-properties}
+ * @see <a href="https://mathhub.info/ulo#size-properties">#size-properties</a>
+ */
+ public static final IRI size_properties;
+
+ /**
+ * {@code https://mathhub.info/ulo#sourceref}
+ * <p>
+ * the URI of the physical location (e.g., file/URI, line, column) of the
+ * source code that introduced the subject.
+ * @see <a href="https://mathhub.info/ulo#sourceref">#sourceref</a>
+ */
+ public static final IRI sourceref;
+
+ /**
+ * {@code https://mathhub.info/ulo#specified-in}
+ * @see <a href="https://mathhub.info/ulo#specified-in">#specified-in</a>
+ */
+ public static final IRI specified_in;
+
+ /**
+ * {@code https://mathhub.info/ulo#specifies}
+ * <p>
+ * The physical organizational item S specifies a knowledge item O, i.e.
+ * S is represented in O
+ * @see <a href="https://mathhub.info/ulo#specifies">#specifies</a>
+ */
+ public static final IRI specifies;
+
+ /**
+ * {@code https://mathhub.info/ulo#statement}
+ * <p>
+ * Statements are declarations of objects that can in principle have
+ * proofs.
+ * @see <a href="https://mathhub.info/ulo#statement">#statement</a>
+ */
+ public static final IRI statement;
+
+ /**
+ * {@code https://mathhub.info/ulo#superseded-by}
+ * <p>
+ * S (a deprecated knowledge item) is superseded by another.
+ * @see <a href="https://mathhub.info/ulo#superseded-by">#superseded-by</a>
+ */
+ public static final IRI superseded_by;
+
+ /**
+ * {@code https://mathhub.info/ulo#theorem}
+ * <p>
+ * Logically (using the Curry-Howard isomorphism), a theorem is a derived
+ * statement, i.e. a declaration with a definiens (this is the proof of
+ * the theorem given in the type).
+ * @see <a href="https://mathhub.info/ulo#theorem">#theorem</a>
+ */
+ public static final IRI theorem;
+
+ /**
+ * {@code https://mathhub.info/ulo#theory}
+ * <p>
+ * A semantically meaningful block of declarations that can be referred
+ * to globally. Examples included MMT theories, Mizar Articles, Isabelle
+ * Locale, and Coq sections.
+ * @see <a href="https://mathhub.info/ulo#theory">#theory</a>
+ */
+ public static final IRI theory;
+
+ /**
+ * {@code https://mathhub.info/ulo#type}
+ * <p>
+ * Types divide their universe into named subsets.
+ * @see <a href="https://mathhub.info/ulo#type">#type</a>
+ */
+ public static final IRI type;
+
+ /**
+ * {@code https://mathhub.info/ulo#typedec}
+ * <p>
+ * A logical paragraph that introduces a type.
+ * @see <a href="https://mathhub.info/ulo#typedec">#typedec</a>
+ */
+ public static final IRI typedec;
+
+ /**
+ * {@code https://mathhub.info/ulo#unimportant}
+ * <p>
+ * S is deemed unimportant (by someone); O is an explanatory string.
+ * @see <a href="https://mathhub.info/ulo#unimportant">#unimportant</a>
+ */
+ public static final IRI unimportant;
+
+ /**
+ * {@code https://mathhub.info/ulo#universe}
+ * <p>
+ * A universe declaration, used e.g. in strong logics like Coq
+ * @see <a href="https://mathhub.info/ulo#universe">#universe</a>
+ */
+ public static final IRI universe;
+
+ /**
+ * {@code https://mathhub.info/ulo#uses}
+ * @see <a href="https://mathhub.info/ulo#uses">#uses</a>
+ */
+ public static final IRI uses;
+
+ /**
+ * {@code https://mathhub.info/ulo#uses-implementation}
+ * @see <a href="https://mathhub.info/ulo#uses-implementation">#uses-implementation</a>
+ */
+ public static final IRI uses_implementation;
+
+ /**
+ * {@code https://mathhub.info/ulo#uses-interface}
+ * @see <a href="https://mathhub.info/ulo#uses-interface">#uses-interface</a>
+ */
+ public static final IRI uses_interface;
+
+ /**
+ * Static initializer
+ */
+ static {
+ ValueFactory vf = SimpleValueFactory.getInstance();
+
+ NAMESPACE_IRI = vf.createIRI(NAMESPACE);
+
+ /***********************
+ * IRI Constant creation
+ ***********************/
+ action_times = vf.createIRI("https://mathhub.info/ulo#action-times");
+ aligned_with = vf.createIRI("https://mathhub.info/ulo#aligned-with");
+ alternative_for = vf.createIRI("https://mathhub.info/ulo#alternative-for");
+ antonym = vf.createIRI("https://mathhub.info/ulo#antonym");
+ automatically_proved = vf.createIRI("https://mathhub.info/ulo#automatically-proved");
+ axiom = vf.createIRI("https://mathhub.info/ulo#axiom");
+ check_time = vf.createIRI("https://mathhub.info/ulo#check-time");
+ constructs = vf.createIRI("https://mathhub.info/ulo#constructs");
+ contains = vf.createIRI("https://mathhub.info/ulo#contains");
+ counter_example_for = vf.createIRI("https://mathhub.info/ulo#counter-example-for");
+ crossrefs = vf.createIRI("https://mathhub.info/ulo#crossrefs");
+ declaration = vf.createIRI("https://mathhub.info/ulo#declaration");
+ defines = vf.createIRI("https://mathhub.info/ulo#defines");
+ definition = vf.createIRI("https://mathhub.info/ulo#definition");
+ deprecated = vf.createIRI("https://mathhub.info/ulo#deprecated");
+ derived = vf.createIRI("https://mathhub.info/ulo#derived");
+ docref = vf.createIRI("https://mathhub.info/ulo#docref");
+ example = vf.createIRI("https://mathhub.info/ulo#example");
+ example_for = vf.createIRI("https://mathhub.info/ulo#example-for");
+ experimental = vf.createIRI("https://mathhub.info/ulo#experimental");
+ external_size = vf.createIRI("https://mathhub.info/ulo#external-size");
+ file = vf.createIRI("https://mathhub.info/ulo#file");
+ folder = vf.createIRI("https://mathhub.info/ulo#folder");
+ formalizes = vf.createIRI("https://mathhub.info/ulo#formalizes");
+ function = vf.createIRI("https://mathhub.info/ulo#function");
+ generated_by = vf.createIRI("https://mathhub.info/ulo#generated-by");
+ hypernym = vf.createIRI("https://mathhub.info/ulo#hypernym");
+ hyponym = vf.createIRI("https://mathhub.info/ulo#hyponym");
+ implementation_uses = vf.createIRI("https://mathhub.info/ulo#implementation-uses");
+ implementation_uses_implementation_of = vf.createIRI("https://mathhub.info/ulo#implementation-uses-implementation-of");
+ implementation_uses_interface_of = vf.createIRI("https://mathhub.info/ulo#implementation-uses-interface-of");
+ important = vf.createIRI("https://mathhub.info/ulo#important");
+ inductive_on = vf.createIRI("https://mathhub.info/ulo#inductive-on");
+ inspired_by = vf.createIRI("https://mathhub.info/ulo#inspired-by");
+ instance_of = vf.createIRI("https://mathhub.info/ulo#instance-of");
+ inter_statement = vf.createIRI("https://mathhub.info/ulo#inter-statement");
+ interface_uses = vf.createIRI("https://mathhub.info/ulo#interface-uses");
+ interface_uses_implementation_of = vf.createIRI("https://mathhub.info/ulo#interface-uses-implementation-of");
+ interface_uses_interface_of = vf.createIRI("https://mathhub.info/ulo#interface-uses-interface-of");
+ internal_size = vf.createIRI("https://mathhub.info/ulo#internal-size");
+ justifies = vf.createIRI("https://mathhub.info/ulo#justifies");
+ last_checked_at = vf.createIRI("https://mathhub.info/ulo#last-checked-at");
+ library = vf.createIRI("https://mathhub.info/ulo#library");
+ library_group = vf.createIRI("https://mathhub.info/ulo#library-group");
+ logical = vf.createIRI("https://mathhub.info/ulo#logical");
+ mutual_block = vf.createIRI("https://mathhub.info/ulo#mutual-block");
+ name = vf.createIRI("https://mathhub.info/ulo#name");
+ nyms = vf.createIRI("https://mathhub.info/ulo#nyms");
+ organizational = vf.createIRI("https://mathhub.info/ulo#organizational");
+ para = vf.createIRI("https://mathhub.info/ulo#para");
+ paratype = vf.createIRI("https://mathhub.info/ulo#paratype");
+ phrase = vf.createIRI("https://mathhub.info/ulo#phrase");
+ physical = vf.createIRI("https://mathhub.info/ulo#physical");
+ predicate = vf.createIRI("https://mathhub.info/ulo#predicate");
+ primitive = vf.createIRI("https://mathhub.info/ulo#primitive");
+ proof = vf.createIRI("https://mathhub.info/ulo#proof");
+ proposition = vf.createIRI("https://mathhub.info/ulo#proposition");
+ revision = vf.createIRI("https://mathhub.info/ulo#revision");
+ rule = vf.createIRI("https://mathhub.info/ulo#rule");
+ same_as = vf.createIRI("https://mathhub.info/ulo#same-as");
+ section = vf.createIRI("https://mathhub.info/ulo#section");
+ see_also = vf.createIRI("https://mathhub.info/ulo#see-also");
+ similar_to = vf.createIRI("https://mathhub.info/ulo#similar-to");
+ size_properties = vf.createIRI("https://mathhub.info/ulo#size-properties");
+ sourceref = vf.createIRI("https://mathhub.info/ulo#sourceref");
+ specified_in = vf.createIRI("https://mathhub.info/ulo#specified-in");
+ specifies = vf.createIRI("https://mathhub.info/ulo#specifies");
+ statement = vf.createIRI("https://mathhub.info/ulo#statement");
+ superseded_by = vf.createIRI("https://mathhub.info/ulo#superseded-by");
+ theorem = vf.createIRI("https://mathhub.info/ulo#theorem");
+ theory = vf.createIRI("https://mathhub.info/ulo#theory");
+ type = vf.createIRI("https://mathhub.info/ulo#type");
+ typedec = vf.createIRI("https://mathhub.info/ulo#typedec");
+ unimportant = vf.createIRI("https://mathhub.info/ulo#unimportant");
+ universe = vf.createIRI("https://mathhub.info/ulo#universe");
+ uses = vf.createIRI("https://mathhub.info/ulo#uses");
+ uses_implementation = vf.createIRI("https://mathhub.info/ulo#uses-implementation");
+ uses_interface = vf.createIRI("https://mathhub.info/ulo#uses-interface");
+ }
+
+ public ULO() {
+ // To enable service discovery to succeed, even though this is a static class
+ }
}
--
GitLab