Class for reducing a conjunction of predicate literals using a set of
known literals (facts).
Class for reducing a conjunction of predicate literals using a set of
known literals (facts). This reduction can be done modulo the axiom of
functionality (for predicates encoding functions or partial functions), and
then potentially replaces predicate literals with simple equations.
Class for reducing a conjunction of predicate literals using a set of known literals (facts). This reduction can be done modulo the axiom of functionality (for predicates encoding functions or partial functions), and then potentially replaces predicate literals with simple equations.