2.1

• add logtk.arith sub-library, using either zarith or num
• implemented two new calculi (with corresponding term orders):
  1. Superposition with first-class Booleans [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_22]
  2. Superposition for full HOL [https://link.springer.com/chapter/10.1007/978-3-030-79876-5_23]
• old 'Case' rules are removed and replaced with corresponding 'BoolHoist' rules
• a new system for selection of Boolean subterms (--bool-select)
• many modes for Boolean reasoning (--boolean-reasoning)
• a whole set of SAT-inspired pre- and inprocessing techniques:
  1. Blocked clause elimination
  2. Nonsingular predicate elimination with definition set recognition
  3. Hidden literal elimination
  4. Quasipure literal elimination
• fixed various issues in handling clause weight, priority and literal selection heuristics
• improved communication with backend
• better (complete) support for renaming common subformulas
• profiling that emits catapult traces (if env contains TEF=1)

2.0

Release with the full power of higher-order and booleans as described in this paper.

1.6

This version contains major improvements from years of work on higher-order extensions to Superposition, including a new HO unification derived from JP unif. See papers on https://matryoshka-project.github.io/ 💃

1.5.1

upgrade on 1.5 with bugfixes, and more up-to-date dependencies (in particular, Iter and Msat).

(self-contained bundle with scripts to install opam and the dependencies is attached)

1.5

stable release