How to load multiple theories

[vasily-kartashov]

I am looking for a way to load multiple theories. In my case I only want an app application.prolog loaded after the prelude.prolog has been loaded.

ClassicSolverFactory.INSTANCE.mutableSolverWithDefaultBuiltins accepts at most two theories (static and dynamic) which seem like they are used for something else.

[gciatto]

There are 2 ways to load multiple theories into a solver:

• either you concatenate them all via the Theory.plus operator, and then you crate a solver out of the whole concatenated theory
• or you crate an empty MutableSolver and you load each theory via the Mutable Solver.appendStaticKb method

The difference among static and dynamic KBs is very important as well.

Clauses in the dynamic KB can be affected by the retract- and assert-like predicates. Clauses in the static KB cannot. So in the general case you may want to lead theories parsed from file into the static KB, as this is the usual Prolog way of consulting theory files