Theory
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).
Theory is deliberately a thin, Prolog-flavoured façade: how clauses are actually stored, searched and mutated is delegated to a ClauseCollection (see the it.unibo.tuprolog.collections package) chosen at construction time. Two independent axes of variation exist, both hidden behind this same interface:
mutable vs. immutable: a plain
Theoryis a persistent data structure — everyassertA/assertZ/retractreturns a newTheory, leavingthisuntouched; a MutableTheory (obtained via toMutableTheory) edits itself in place instead, which is cheaper when a program asserts/retracts clauses very frequently (e.g. a Prologdynamicpredicate).indexed vs. listed: an indexed theory (the default, see indexedOf) keeps clauses in a discrimination-tree-like structure (see
it.unibo.tuprolog.collections.rete.custom.ReteTree) indexed by directive-vs-rule, functor, arity and first-argument shape, trading memory and update cost for fast lookup; a listed theory (see listedOf) is a thin wrapper around an ordered clause list, cheap to build and to keep in insertion order, but linear to query (eachgetscans and unifies against every clause). A knowledge base that is queried far more often than it is changed (a typical static, "library" theory) benefits from indexing; one that is asserted/retracted on nearly every resolution step, or kept small, may not be worth indexing at all — which is exactly why solvers (see:solve) build their static knowledge base with of (indexed) and their dynamic one with listedOf.
Example — building a small theory and querying it:
val theory =
Theory.indexedOf(
Unificator.default,
Fact.of(Struct.of("parent", Atom.of("alice"), Atom.of("bob"))),
Fact.of(Struct.of("parent", Atom.of("bob"), Atom.of("carol"))),
)
val goal = Struct.of("parent", Var.of("Who"), Atom.of("bob"))
theory[goal].toList() // rules/facts whose head *might* unify with `parent(Who, bob)`See also
Inheritors
Properties
Whether this Theory supports in-place mutation; true for MutableTheory, false otherwise.
Whether this Theory is full or not
Functions
Checks if given clause is contained in this theory
Checks if clauses exist in this theory having the specified indicator as head.
Checks if given clause is present in this theory
Checks whether this theory and other contain the same clauses, in the same order. If useVarCompleteName is true, variables are compared also by their (possibly generated) complete name, rather than only by their position within each clause.
Adds all the clauses of the given theory after all the clauses of this one, returning the resulting Theory (as a new instance, unless is emptyTheory.isEmpty).
Tries to delete the first clause in this theory unifying against the given clause, returning a RetractResult.Success wrapping the resulting Theory and the removed clause, or a RetractResult.Failure wrapping this same theory if no clause matched.
Tries to delete a clause whose head unifies against the given head; equivalent to retract(Rule.of(head, _))
Tries to delete, from this theory, one clause unifying against each of the given clauses patterns.
Returns a Theory with the same clauses as this one, but using the given unificator to match them.
Returns an immutable Theory with the same clauses (and Unificator) as this one; this, if it already is one.
Returns a MutableTheory with the same clauses (and Unificator) as this one; this, if it already is one.
An enhanced toString that prints the theory in a Prolog program format, if asPrologText is true