Semantic Web reasoners are powerful tools that allow the extraction of implicit information from RDF data. This information is reachable through the definition of ontologies and/or rules provided to the reasoner. To achieve this, various algorithms are used by different reasoners. In this paper, we explain how state space search can be applied to create a backward-chaining rule-based reasoner. By using the OWL-profiles (especially OWL 2 RL), DL-based reasoning becomes possible. State space search is an approach used in the Artificial Intelligence domain that solves problems by modeling them as a graph and searching (using diverse algorithms) for solutions within this graph. State space search offers inherent proof generation and the ability to plug in different search algorithms to determine the characteristics of the reasoner such as: speed, memory or ensuring shortest proof generation.
Semantic reasoners are used to infer new knowledge from existing knowledge. Ideally, a
verifiable proof can be provided for each inference. Despite the importance of proofs for
the trust component in the Semantic Web Stack1 envisioned by Tim Berners-Lee, proof
generation is only supported by very few reasoners (such as EYE [
Algorithms used by current reasoners are: Euler path detection (EYE), tableaux
(Pellet [
By plugging different search algorithms into state space search, the characteristics of
the reasoner can be tweaked. This includes speed and memory usage, but also the ability
to generate the shortest proof, a property not directly supported by any other reasoner.
For applications such as RESTdesc [
State space search transforms a problem context into a directed state graph, where each vertex represents a certain state of the context being modeled and the edges are determined by what is considered a valid transition between states. In this graph, both the starting situation and solution are represented by one or more vertices. This graph may or may not be materialized for a specific problem. Path finding is one of the more well-known applications of state space search.
The process of solving the problem consists of finding a path between the starting vertex and one of the solution vertices. This is done by creating a search tree that explores the state graph. The search tree and the state graph are separate concepts, as the search tree tracks information about the solution being constructed. In the example of path finding the state graph coincides with the graph being navigated where each vertex represents a location. The search tree tracks how each node was reached (one path may be better than the others).
The performance of state space search depends on the algorithm used to construct the
search tree. Depending on the requirements, a suitable algorithm may be selected.
Wellknown algorithms include: A*, IDA* [
Although any form of backward-chaining reasoning could be considered as a form of state space search, it has not been examined as such in current literature to the best of our knowledge. 3
Rule-based reasoners differ from ontological reasoners since they are configured to only use a specified set of rules rather than the OWL 2 specification. Luckily, big parts of OWL 2 can still be used for rule-based reasoning through OWL 2 RL, a subset of OWL 2 that can be expressed in rules.
In rule-based reasoners, data and rules are both provided as input. Listing 1.1 and
1.2 list example rules and data in Notation3 (N3) [
1 @prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>. 2 @prefix : <http://www.example.com/>. 3 {?x a :CoolPerson} => {?x :has :sunglasses}. # Rule 1 4 {?x a ?Sub. ?Sub rdfs:subClassOf ?Super} => {?x a ?Super}. # Rule 2
Listing 1.1. Example rules in N3. 1 @prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>. 2 @prefix : <http://www.example.com/>. 3 :MovieStar rdfs:subClassOf :CoolPerson. 4 :Researcher rdfs:subClassOf :CoolPerson. 5 :alice a :Researcher.
Listing 1.2. Example facts in N3.
Using state space search, we can design a backward-chaining rule-based reasoner that allows us to prove given statements. Each node in the search tree contains a number of statements that are yet to be confirmed. Starting from the root node which contains the statement to be proven, the children of each node represent the different ways to confirm a remaining statement from its parent. This can be done by finding the statement in the known facts, or by applying a rule that proves the statement given that its prerequisites are satisfied, thereby introducing new statements to be proven. A solution is found when a node is reached where no remaining statements are to be proven. The path from the root node to the solution acts as the corresponding proof. Figure 1 demonstrates an example search tree.
In more realistic examples, the search tree might contain millions of nodes. The chosen search algorithm determines how much of the search tree will be constructed before a solution is found. 4
By allowing to change the search algorithm, it is possible to tweak the characteristics of the reasoner. For example, it would be possible to guarantee that the shortest possible proof is found by using a variant of the A* algorithm. If memory is the most important factor, a variant of depth first search could be used. This choice does not have to be made in advance, it could be specified through configuration for each reasoner run.
Because multiple search algorithms are supported, it is easy to tweak the performance
of the reasoner to specific use cases. It is also possible to create context agnostic
heuristics to further improve these search algorithms by analyzing the common patterns
of previously generated proofs. This could be similar to the approach used by Arndt
et al. [
Finally, the usage of different approaches to reasoning is not just interesting from an academic point of view. It is a vital part of the trust component in the Semantic Web Stack, where exchangeable proofs should be checked by independent reasoners using different algorithms. 5
In this paper, we explained our proposal to apply state space search to create a backwardchaining rule-based semantic reasoner. Using different algorithms is important to enable trust, but using state space search offers other specific advantages: 1) it is trivial to construct proofs during reasoning due to the nature of state space search; 2) the ability to switch between different search algorithms to determine the characteristics of the reasoner, such as guaranteeing the generation of the shortest proof; 3) the potential gain of automatically updating search heuristics based on previous queries.