Module sld 

Structs

Graph

LiteralOrigin

A literal origin can be uniquely identified through its source clause and its index in the clause body

Proof

A proof tree consist of

SLDResult

Result of building the SLD tree.

Tree

An SLD tree consists of

Enums

ClauseId

In this usage, a ‘clause’ represents some method of resolution.

ResolutionError

Traits

Auxiliary

Functions

proofs

sld

Returns a tree that contains both successful and failed paths, also, any resolution errors. To save on memory usage, can avoid storing the failed paths by passing false to store_full_tree.

solutions

tree_from_modusfile