Package-level declarations

A TheoryFactory that produces Theory/MutableTheory instances backed by an indexed data structure (see it.unibo.tuprolog.collections.rete.custom.ReteTree): clauses are discriminated by directive-vs-rule, functor, arity and first-argument shape, so retrieval only re-checks the (typically small) subset of clauses that could actually unify with a goal, at the cost of extra bookkeeping on every insertion/removal. This is the right choice for knowledge bases that are built once (or rarely changed) and queried many times — e.g. a solver's static knowledge base.

A TheoryFactory that produces Theory/MutableTheory instances backed by a plain ordered list of clauses: cheap to build and to keep in insertion order, but every retrieval degenerates to a linear scan with a per-clause unification check. This is the right choice for knowledge bases that change on (almost) every resolution step, or are small enough that indexing overhead is not worth paying — e.g. a solver's dynamic knowledge base.

A Theory that mutates itself in place: assertA/assertZ/retract/abolish (and their plus shorthands) change and return this, instead of building a fresh Theory. This is cheaper than the persistent-data- structure behaviour of a plain Theory when clauses are asserted/retracted very frequently — e.g. to back a Prolog dynamic knowledge base updated on (almost) every resolution step — at the cost of the usual aliasing caveat: every reference to a MutableTheory observes every mutation performed through any other reference.

The outcome of a Theory.retract/Theory.retractAll operation: either Success, carrying the resulting theory and the clauses that were actually removed, or Failure, carrying the theory unchanged because no clause matched. Modelled as a sealed hierarchy (rather than, say, a nullable result) so that callers must handle both cases explicitly, mirroring how Prolog's own retract/1 can succeed or simply fail.

A Prolog knowledge base: an ordered collection of Clauses (facts, rules and directives) that can be queried by unification against a goal, and grown or shrunk with the usual ISO-inspired vocabulary (assertA/assertZ/retract/abolish).

A factory of Theory/MutableTheory instances, all sharing the same backing data structure (e.g. indexed or listed, see IndexedTheoryFactory and ListedTheoryFactory) and, by default, the same unificator.