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.

AuthorJohn D. Ramsdell <ramsdell@mitre.org>
LicenseBSD
Published
Homepagehttps://github.com/ramsdell/chase
Issue Trackerhttps://github.com/ramsdell/chase/issues
MaintainerJohn D. Ramsdell <ramsdell@mitre.org>
Dependencies
Source [http] https://github.com/ramsdell/chase/archive/1.3.tar.gz
sha256=6a005e56644ea629f4d24516304f1b30f2e49c1e1a49349d81f8a2fa3d74aa9d
md5=3d3d9475cd9d84a68df10d9bf1197ac7
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/chase/chase.1.3/opam
No package is dependent