Last updated
Last updated
Before we come to the topic on defining axioms, it is necessary to gain insight on the way that the axiom processing machinery has been build (, ).
Inferencing is the procedure in which new triples are systematically added to a graph based on patterns in existing triples. Three of the most common reasoning methods are forward and backward chaining, and verification. The first two methods leverage “if-then” rules, whereas the latter verifies the satisfiability of axioms.
Take as example the following two simple rules:
“IF it is raining THEN the ground is wet”;
“IF cargo is of Dangerous Nature THEN insert the hazard code with value 1".
In forwards chaining processes, the reasoner matches the IF clause of the rule and when a match is found, it asserts the THEN clause. So if the reasoner finds the statement "the nature of cargo is dangerous" in the knowledge base, it can apply the rule mentioned above to deduce that the danger code must be 1. Forwards chaining is data driven and can be used to draw all of the conclusions one can deduce from an initial state and a set of inference rules. To that end, the reasoner must execute all consequents, i.e., the THEN-part, of the rules the antecedents of which, i.e., the IF-part of the clause, are matched in the knowledge base.
Backward chaining works in other direction. It is often viewed as goal directed. Suppose that the goal is to determine whether or not "the ground is wet". A backward chaining approach would look to see if the statement, “the ground is wet”, matches any of the consequent of the rules. If so, it will subsequently determine (i) whether or not the antecedent "it is raining" is a currently available fact in the knowledge base, or (ii) whether there is a way to deduce the antecedent of the rule. For making the latter deduction it will start another backward chaining cycle, now to see whether the statement "it is raining" (originally the antecedent of rule 1) exists as consequent for another rule, the antecedent of which can be found as currently available fact. This is repeated until an antecedent of the chained rules is currently available as fact (and hence, deducing the new fact "the ground is wet"), or no more rules can be found that carries a consequent that matches the current antecedent under deduction (and hence, deducing unknown because open world deduction is assumed).
The third type of reasoning, tableaux reasoning, is based on a technique that checks for satisfiability of a finite set of axioms. The objective of its proofing method is to show that the negation of a formula cannot be satisfied. From that it follows that the orginal, non-negated rule must be a logical truth. To that end, the reasoner must be complete in establishing that: for all possibilities in rules that logically follow from the negation of the original rule; and all available facts related to or deduced from those rules, an inconsistency results. That means that for rule 2 above, it will assert that it is NOT the case that the "cargo is of Dangerous Nature", and then work to determine whether an inconsistency can be achieved, with asserted and currently available facts alike. One application of the method is for validation and consistency checks, that is, the process by which triples in the data graph (asserted triples) are systematically checked against some predefined constraints (inference rules) for finding missing data and ensure the consistency and integrity of the knowledge base.
A semantic reasoner, reasoning engine, rules engine, or simply a reasoner, is a piece of software able to infer logical consequences from a set of asserted facts or axioms. Its inference engine itself is a component of the reasoner that applies logical rules to the knowledge base to deduce new information. Some main components are required for providing a generic reasoning capability. This has been depicted below, with its 6 components shortly described.
Inference rules are commonly specified by means of an ontology language - often a description logic language - or a constraint language. In our running examples, the IF clause sentence, the antecedent contains the axiom. The axiom is a statement that is taken to be true, to serve as a premise or starting point for further reasoning. These axioms can be represented in the ontology language using OWL, and RDFs and shacl. See some examples of the Owl axioms
An Inference Engine applies inference rules to the knowledge base, viz. the schema and data triples. The data triples are either delivered facts or facts that have been inferred by one of the inference rules; no semantic distinction exists between the two. The inferencing process continues until the data set stabilises, i.e., no more triples can be inferred from the particular set of inference rules on the basis of the available data triples.
Query Engine: Once the inferencing has been stabilised, the data set is allowed to be queried. In a separate task, a SPARQL query engine runs over the resulting triple store for mapping the a asserted triples to a required pattern (defined in the sparql body).
With Knowledge Base one refers to either a triple store or a graph database containing the ABOX, that is, asserted triples. Data from various sources and format must get transformed into triples (via a mapping to the ontology) and merged with the knowledge base.
Applications can only interact with the knowledge base through its query interface, or endpoint.
External data sources (databases, web pages, documents, images and all other digital forms of data) can only be taken into account by the reasoner once its data has been converted into triples (then considered asserted triples) or by inserting triples that represent particular facts on that external data, e.g., <ex:image4285> <:contains> <:Person1234> .
Purpose: make your model more complete by defining general truths.
Formal axioms are used in ontologies to model sentences that are always true, while functions represent special case of relations. These may help you ontology be more precise and complete.
Work in Progress
How do we define those? What are our guidelines? What recommendations do we have? What are the guiding questions?
IF it is useful THEN consider it