package 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.