Interface Proof


  • public interface Proof

    Represents a proof tree. Proof tree provides an explanation for an inference or an inconsistency in a hierarchical structure. A proof may simply represent an assertion in the database. More complex proofs are nested where the immediate children of a proof provides a concise explanation for the expression associated with that proof.

    An example proof (serialized by ProofWriter) looks like as follows:

     INFERRED :Alice rdf:type :Employee
         ASSERTED :Manager rdfs:subClassOf :Employee
         INFERRED :Alice rdf:type :Manager
             ASSERTED :Alice :supervises :Bob 
             ASSERTED :supervises rdfs:domain :Manager
     
    Since:
    2.0
    Version:
    6.0
    Author:
    Evren Sirin
    • Method Summary

      All Methods Instance Methods Abstract Methods 
      Modifier and Type Method Description
      Proof getAlternate()
      Returns the alternate proof.
      java.lang.Iterable<Proof> getChildren()
      Returns the child nodes.
      Axiom getExpression()
      Returns the expression associated with this proof instance.
      java.lang.Iterable<Axiom> getExpressions()
      Returns the union of all asserted expressions in this proof tree.
      java.lang.Iterable<Axiom> getExpressions​(com.complexible.stardog.reasoning.ProofType theType)
      Returns the union of all expressions for all nodes in this proof tree with the given type.
      java.util.Set<IRI> getNamedGraphs()
      Returns the URIs of named graphs where the expression for this proof node is asserted if the type is asserted or empty set otherwise.
      java.lang.Iterable<Statement> getStatements()
      Returns the union of all asserted statements in this proof tree.
      java.lang.Iterable<Statement> getStatements​(com.complexible.stardog.reasoning.ProofType theType)
      Returns the union of all statements for all nodes in this proof tree with the given type.
      com.complexible.stardog.reasoning.ProofType getType()
      Returns the type of this proof instance.
      boolean hasAlternate()
      Returns true if the proof has an alternate.
      boolean hasChildren()
      Returns true if this element has any children or false otherwise.
      java.lang.String toString​(java.lang.Iterable<Namespace> theNamespaces)
      Returns the string representation of this proof using the given namespaces for abbreviations.
    • Method Detail

      • getExpression

        Axiom getExpression()
        Returns the expression associated with this proof instance.
        Returns:
        expression associated with this proof instance
      • getType

        com.complexible.stardog.reasoning.ProofType getType()
        Returns the type of this proof instance.
        Returns:
        proof type
      • getNamedGraphs

        java.util.Set<IRI> getNamedGraphs()
        Returns the URIs of named graphs where the expression for this proof node is asserted if the type is asserted or empty set otherwise. If the expression is asserted in the default graph, the special default graph URI will be returned. This set might be empty if the explainer was not configured to compute named graphs.
        Returns:
        named graphs of this proof
      • getChildren

        java.lang.Iterable<Proof> getChildren()
        Returns the child nodes.
        Returns:
        the child proofs
      • hasChildren

        boolean hasChildren()
        Returns true if this element has any children or false otherwise.
        Returns:
        true if this element has any children or false otherwise
      • getAlternate

        Proof getAlternate()
        Returns the alternate proof. An alternate proof is another way to explain the inference.
        Returns:
        alternate proof or null if there are not alternatives
      • hasAlternate

        boolean hasAlternate()
        Returns true if the proof has an alternate.
        Returns:
        true if this element has an alterantive or false otherwise
      • getExpressions

        java.lang.Iterable<Axiom> getExpressions()
        Returns the union of all asserted expressions in this proof tree.
        Returns:
        the union of all asserted expressions in this proof tree
      • getStatements

        java.lang.Iterable<Statement> getStatements()
        Returns the union of all asserted statements in this proof tree.
        Returns:
        the union of all asserted statements in this proof tree
      • getExpressions

        java.lang.Iterable<Axiom> getExpressions​(com.complexible.stardog.reasoning.ProofType theType)
        Returns the union of all expressions for all nodes in this proof tree with the given type.
        Returns:
        the union of all expressions for all nodes in this proof tree with the given type
      • getStatements

        java.lang.Iterable<Statement> getStatements​(com.complexible.stardog.reasoning.ProofType theType)
        Returns the union of all statements for all nodes in this proof tree with the given type.
        Returns:
        the union of all statements for all nodes in this proof tree with the given type
      • toString

        java.lang.String toString​(java.lang.Iterable<Namespace> theNamespaces)
        Returns the string representation of this proof using the given namespaces for abbreviations.
        Returns:
        the string representation of this proof using the given namespaces for abbreviations