List of Modules¶
The most uptodate reference to the list of modules is in the _oasis
file
at the root of the project. This file describes how to build parts of the
library.
In this document we give a highlevel view of what every module in Logtk
does.
Main Library¶
The main library contains a single packed module, Logtk
, which depends
only on zarith
(a wrapper around GMP used
for arbitraryprecision arithmetic) and unix
(the standard OCaml
wrapper to the Posix APIs). This module
contains other modules, for instance Logtk.FOTerm
for representing
firstorder 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 (usingZarith
).ScopedTerm
: common internal representation for terms, formulas, etc. that handles De Bruijn indices, substitutions, and hashconsing.PrologTerm
: the dual ofScopedTerm
, an untyped AST with locations but no hashconsing nor scoping.FOTerm
: firstorder typed terms (built on top ofScopedTerm
)HOTerm
: higherorder typed termsFormula
: formulas parametrized by the terms at their leaves.Formula.FO
: firstorder formulas (with typed terms).
Type
: polymorphic types with explicit quantification, built on top of
ScopedTerm
, used byFOTerm
andHOTerm
.
Unif
: unification algorithms, both unary and nary.Unif.FO
: specialization forFOTerm
Unif.Ty
: specialization forType
 similar submodules.
Substs
: substitutions on free variables for types and terms.DBEnv
: De Bruijn environments for bound variables.Signature
: map from symbols to typesTypeInference
: HindleyMilnerlike type inference algorithm, that convertsPrologTerm
to typed terms and formulas.Precedence
: total ordering on symbols.Ordering
: orderings on terms, including LPO and KBO (parametrized byPrecedence
).Position
: positions in terms (paths in trees)Cnf
: transformation of formulas into Clause Normal FormIndex
: definition of term index signatures. Related modules:Dtree
: perfect discrimination tree, for rewritingNPDtree
: nonperfect discrimination tree, for rewriting and term indexingFingerprint
: fingerprint term indexingFastFingerprint
: attempt (failed for now) to makeFingerprint
fasterFeatureVector
: featurevector indexing for subsumption
Rewriting
: rewriting on terms, ordered rewriting, formula rewriting.FormulaShape
: detection of some specific formulas (definitions...).Skolem
: skolemization and definitional CNF.Lambda
: lambdacalculus (beta reduction) on higherorder terms.Transform
: computation of fixpoints over transformations of formulasMultiset
: low level multiset of elements, with multiset orderingCongruence
: 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.
Parsers¶
This sublibrary is optional and will only be built if
menhir (an
excellent parser generator for OCaml) is installed. Currently it
contains parsers for two file formats. Again the library is
a packed module Logtk_parsers
(e.g. Logtk_parsers.Ast_tptpt
).
Logtk_parsers
TPTP
:Trace_tstp
: proof traces from TSTP provers.CallProver
: call a TSTP prover on a problem.Parse_tptp
: TPTP parserLex_tptp
: TPTP lexerAst_tptp
: AST yielded by the parserUtil_tptp
: higherlevel interface to the TPTP parser (the one to use)
HO
(an adhoc format for higherorder terms with multisets and extensible records):

Parse_ho
: parser for a simple HigherOrder format Lex_ho
: lexer for a simple HigherOrder format Ast_ho
: AST yielded byParse_ho
MetaProver¶
A prover that reasons about features of the problem at hand: higherlevel
properties of symbols, algebraic structures, etc. See there
for more details. The library is packed into Logtk_meta
.
Logtk_meta
Encoding
: encoding of formulas and terms into HO terms.Reasoner
: forwardchaining reasoner on metalevel facts.Plugin
: bridge between HO terms and their prooflevel meaning.Prover
: general interface to the metaprover.
Arbitrary Instances¶
This module is only built if qcheck
(a random propertytesting library similar to Haskell’s QuickCheck) is
installed. It provides random generators for terms, formulas, etc.
The library is packed into Logtk_arbitrary
.
Logtk_arbitrary
(random generators forqcheck
randomtesting, optional)ArTerm
: generation of random termsArForm
: random first order formulasArType
: random typesArSignature
: random signaturesArSymbol
: random symbolsArPattern
: random metapatterns