chaseversion
Model finder for geometric theories using the chase
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.
| Author | John D. Ramsdell <ramsdell@mitre.org> |
|---|---|
| License | BSD-3-Clause |
| Published | |
| Homepage | https://github.com/ramsdell/chase |
| Issue Tracker | https://github.com/ramsdell/chase/issues |
| Maintainer | John D. Ramsdell <ramsdell@mitre.org> |
| Dependencies | |
| Source [http] | https://github.com/ramsdell/chase/archive/1.5.tar.gz sha256=61d6a0e67790fe8200e552df1cda2004a8eeb7073d59a4640a657e995ededf72 md5=d96e17e1c932392d012e3ea1cbdf1285 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/chase/chase.1.5/opam |
No package is dependent
