## Main Library¶

The main library contains a single packed module, `Logtk`, which depends
only on `zarith` (a wrapper around GMP used
for arbitrary-precision arithmetic) and `unix` (the standard OCaml
wrapper to the Posix APIs). This module
contains other modules, for instance `Logtk.FOTerm` for representing
first-order terms. It is often useful to rename modules prior to their
use, for instance

```
module T = Logtk.FOTerm
module P = Logtk.Position
```

This technique allows to keep identifiers short, without using the `open`
directive that makes code hard to read (one cannot easily find which opened
module some identifier comes from).

`Logtk``Symbol`: representation of logical constants, including text symbols and numeric symbols (using`Zarith`).`ScopedTerm`: common internal representation for terms, formulas, etc. that handles De Bruijn indices, substitutions, and hashconsing.`PrologTerm`: the dual of`ScopedTerm`, an untyped AST with locations but no hashconsing nor scoping.`FOTerm`: first-order typed terms (built on top of`ScopedTerm`)`HOTerm`: higher-order typed terms`Formula`: formulas parametrized by the terms at their leaves.`Formula.FO`: first-order formulas (with typed terms).

`Type`: polymorphic types with explicit quantification, built ontop of

`ScopedTerm`, used by`FOTerm`and`HOTerm`.

`Unif`: unification algorithms, both unary and n-ary.`Unif.FO`: specialization for`FOTerm``Unif.Ty`: specialization for`Type`- similar sub-modules.

`Substs`: substitutions on free variables for types and terms.`DBEnv`: De Bruijn environments for bound variables.`Signature`: map from symbols to types`TypeInference`: Hindley-Milner-like type inference algorithm, that converts`PrologTerm`to typed terms and formulas.`Precedence`: total ordering on symbols.`Ordering`: orderings on terms, including LPO and KBO (parametrized by`Precedence`).`Position`: positions in terms (paths in trees)`Cnf`: transformation of formulas into*Clause Normal Form*`Index`: definition of term index signatures. Related modules:`Dtree`: perfect discrimination tree, for rewriting`NPDtree`: non-perfect discrimination tree, for rewriting and term indexing`Fingerprint`: fingerprint term indexing`FastFingerprint`: attempt (failed for now) to make`Fingerprint`faster`FeatureVector`: feature-vector indexing for subsumption

`Rewriting`: rewriting on terms, ordered rewriting, formula rewriting.`FormulaShape`: detection of some specific formulas (definitions...).`Skolem`: skolemization and definitional CNF.`Lambda`: lambda-calculus (beta reduction) on higher-order terms.`Transform`: computation of fixpoints over transformations of formulas`Multiset`: low level multiset of elements, with multiset ordering`Congruence`: simple congruence closure on terms (decides ground equality)and many helpers modules that can be found in

`src/base/lib/`, including locations, iterators, hashconsing, combinators, etc.