package chase

  1. Overview
  2. No Docs
Model finder for geometric theories using the chase

Install

Authors

Maintainers

Sources

1.4.tar.gz
md5=937e96273bb2bea1be60a3e7d2672fd9

Description

Chase is a model finder for first order logic with equality. It finds minimal models of a theory expressed in geometric form, where functions in models may be partial. A formula is in geometric form if it is a sentence consisting of a single implication, the antecedent is a conjunction of atomic formulas, and the consequent is a disjunction. Each disjunct is a possibly existentially quantified conjunction of atomic formulas. A function is partial if it is defined only on a proper subset of its domain.

Published: 27 Nov 2020

Dependencies (3)

  1. dune >= "1.1"
  2. getopt
  3. ocaml >= "4.05"

Dev Dependencies

None

Used by

None

Conflicts

None