Package com.complexible.stardog.reasoning

# 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

  Modifier and Type
  Method
  Description
  `Proof`
  `getAlternate()`
  Returns the alternate proof.
  `Iterable<Proof>`
  `getChildren()`
  Returns the child nodes.
  `Axiom`
  `getExpression()`
  Returns the expression associated with this proof instance.
  `Iterable<Axiom>`
  `getExpressions()`
  Returns the union of all asserted expressions in this proof tree.
  `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.
  `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.
  `Iterable<Statement>`
  `getStatements()`
  Returns the union of all asserted statements in this proof tree.
  `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.
  `String`
  `toString(Iterable<Namespace> theNamespaces)`
  Returns the string representation of this proof using the given namespaces for abbreviations.

- ## Method Details

  - ### 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

    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

    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

    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

    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

    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

    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

    String toString(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