Zipperposition Versions Save

An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.

2.1

2 years ago
  • 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

3 years ago

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

1.6

3 years ago

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/ :dancer:

1.5.1

4 years ago

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

5 years ago

stable release