## chaseversion

#### Model finder for geometric theories using the chase

The chase program 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 |

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.2.tar.gz md5=157a6b2be81bdb0afc4cde76b6f0e88a |

Statistics | Installed 5 times last month. |

Edit | https://github.com/ocaml/opam-repository/tree/master/packages/chase/chase.1.2/opam |

No package is dependent