chase

Model finder for geometric theories using the chase
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.

Install
Published
27 Nov 2020
Authors
Maintainers
Sources
1.4.tar.gz
md5=937e96273bb2bea1be60a3e7d2672fd9
Dependencies
dune >= "1.1"
ocaml >= "4.05"
Reverse Dependencies