[Input Syntax] [Structures] [Output Syntax] [Formula Selection Order] [Chase Usage] [Output Visualization] [Chasetree Usage] [Makefile] [Including Files] [Algorithm]

John D. Ramsdell

The MITRE Corporation

Chase is a model finder for first-order logic with equality. It
finds minimal models of a theory expressed in finitary geometric
form, where functions in models may be partial. A formula is
in *finitary geometric form* if it is a finite 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. A sentence
in first-order logic is *finitary geometric* iff it is
logically equivalent to finite set of sentences in finitary
geometric form. Finitary geometric logic is also called coherent
logic.

We will assume familiarity with basic ideas and results from
first-order mathematical logic; notions that are not defined here
are treated in any text on logic with allowances for partial
functions. When a structure `A` satisfies
theory `T`, we write `A` |= `T` and
call `A` a model. The definition of a homomorphism must
account for partial functions.

**Definition:** Let `A` and `B` be
structures. A homomorphism `h` of `A`
into `B` is a function with these properties

- For each
`n`-place predicate`P`,`P`(`a`_{1}, ...,`a`_{n}) in`A`implies`P`(`h`(`a`_{1}), ...,`h`(`a`_{n})) in`B`. - For each
`n`-place function`f`,`f`(`a`_{1}, ...,`a`_{n}) =`a`_{0}in`A`implies`f`(`h`(`a`_{1}), ...,`h`(`a`_{n})) =`h`(`a`_{0}) in`B`.

We write `A` <: `B` when there is a
homomorphism from `A` into `B`.

**Definition:** Model `A` of `T`
is *minimal* iff for all models `B`
of `T`, whenever model `B` <: `A`
then `A` <: `B`.

**Definition:** A set of models `M` is
a *set of support* iff whenever
`B` |= `T` there exists a model `A`
in `M` such that `A` <: `B`.

When given a theory, Chase produces a set of support whenever it terminates successfully. It may produce some models that are not minimal. Chase can also be run in a mode in which it terminates successfully after finding just one model.

The input to Chase is a set of sequents written in a slight variant of Geolog syntax. The syntax is inspired by Prolog. Quantification is implicit and constants and variables are distinguished using capitalization.

A Geolog sequent has the form

A_{1}&A_{2}& ... &A=>_{m}C_{1}|C_{2}| ... |C._{n}

The formula to the left of `=>`

is the antecedent, and
the consequent is to the right. Each
conjunct `A _{i}` in the antecedent is an atomic
formula. The consequent is a disjunction. Each
disjunct

B_{j,1}&B_{j,2}& ... &B_{j,p}

where each conjunct `B _{j,k}` is an atomic
formula. A consequent with no disjuncts is indicated by the
reserve symbol

`false`

. A conjunction with no
conjuncts is indicated by the reserved symbol `true`

.
When the antecedent is true, the tokens `true =>`

may
be omitted. Following Prolog, commas can be used to form
conjunctions and semicolons can be used to form disjunctions.A symbol is a letter followed by a sequence of letters, dollar
signs (`$`

), and underscores (`_`

). An
atomic formula is a predicate symbol (a symbol not capitalized)
applied to a parenthesized sequence of comma separated terms, or
an equality consisting of two terms separated by
the `=`

sign. A term is a variable (a capitalized
symbol), a constant (a symbol not capitalized), or a function
symbol (a symbol not capitalized) applied to a parenthesized
sequence of comma separated terms.

Comments start with `%`

and continue until the end of
the line. An example of a theory for input follows.

% Conference Management author(X) & paper(Y) & assigned(X, Y). author(X) & paper(Y) => read_score(X, Y) | conflict(X, Y). assigned(X, Y) & author(X) & paper(Y) => read_score(X, Y). assigned(X, Y) & conflict(X, Y) => false.

The variables that occur in the antecedent of a sequent are
universally quantified. The variables that occur in
disjunct `B _{j}` and not in the antecedent are
existentially quantified over the disjunct. Thus,

p(X) | q(X).

means (exists `X` `p(X)`) or
(exists `X` `q(X)`) *not*
exists `X` (`p(X)` or `q(X)`).

To specify that `X` is universally quantified in the
consequent, add `X=X` to the antecedent. Thus
for all `X`, `p(X)` is written as:

X = X => p(X).

A Chase structure for theory `T` is a set of facts.
A *fact* is a ground atomic formula that has one of two
forms:

`P`(`c`_{1}, ... ,`c`)_{n}`f`(`c`_{1}, ... ,`c`) =_{m}`c`_{0}

The universe of structure `A` is the least
set `U` of constants such that

`P`(`c`_{1}, ... ,`c`) in_{n}`A`implies`c`_{1}, ... ,`c`in_{n}`U``f`(`c`_{1}, ... ,`c`) =_{m}`c`_{0}in`A`implies`c`_{0}, ... ,`c`in_{m}`U`

Let `C` be the set of constants that occur in
theory `T`. A structure `A` produced by Chase
for theory `T` has the following properties.

- Functions may be partial.
- Each constant in
`C`is the left hand side of a fact. - Equality in
`A`is closed under congruence. - Each element in
`U`is the canonical representative of an equivalence class induced by congruence closure.

% chase version 1.4 % bound = 250, limit = 2000, input_order = false % ******** % author(X) & paper(Y) & assigned(X, Y). % (0) % author(X) & paper(Y) => read_score(X, Y) | conflict(X, Y). % (1) % assigned(X, Y) & author(X) & paper(Y) => read_score(X, Y). % (2) % assigned(X, Y) & conflict(X, Y) => false. % (3) % ******** (0)[] (1,0){0}[assigned(x, y), author(x), paper(y)] (2,1){1}![assigned(x, y), author(x), paper(y), read_score(x, y)] (3,1){1}[assigned(x, y), author(x), conflict(x, y), paper(y)] (4,3){2}[assigned(x, y), author(x), conflict(x, y), paper(y), read_score(x, y)]

A run of Chase produces structures assembled into a tree. The
root of the tree is labeled (0). A label of the form (n, p) gives
the node number of the tree node and its parent. When
structure `A` is the parent of `B`, there exists
a homomorphism from `A` into `B`. Every Chase
step is structure-preserving.

The form {r} records the rule used to produce this structure. A structure marked with ! is a model. Thus in this output, there are two paths explored, <0,1,2> and <0,1,3,4>, and one model found (2).

The second line of the output records the runtime parameters used
to control termination. The program will terminate when the
number of facts in a structure exceeds the size bound or when the
number of structures produced exceeds the step limit. Runtime
parameters can be specified on the command line,
where `-b`

sets the size bound, `-l`

sets
the step limit, and `-i`

sets input order formula
selection. Runtime parameters can also be specified at the
beginning of the input. Within square brackets, write ```
bound
= 66
```

to specify a size bound of 66, write ```
limit =
1024
```

to specify a step limit of 1024, and
write `input_order`

to specify input order formula
selection. Use a comma to separate parameters when more than one
is specified.

[ bound = 66, limit = 1024, input_order ]

Runtime parameters specified in the input take precedence over parameters specified on the command line.

Chase divides formulas into two classes. A formula
is *lightweight* iff it contains at most one disjunct in
its consequent and it contains no existentially quantified
variables. Otherwise, the formula is *heavyweight*. Chase
always tries lightweight formulas before it considers heavyweight
formulas.

To avoid formula starvation, by default, Chase modifies the
formula selection order for either lightweight or heavyweight
formulas at each step. If input order mode
(`-i`

) is selected, the formula selection order does
not change at runtime. Lightweight and heavyweight formulas are
tried in the order they are given in the input source file.

Chase reads a theory from a file or from standard input when no file name is given on the command line. When the input file name has the extension ".md", the input syntax is treated as Markdown, and Chase input is extracted from fenced code blocks. By default, the output is sent to standard output. When an error occurs, such as when a bound or limit is exceeded, the error message goes to standard error and the program exits with status 1.

$ chase -h Usage: chase [OPTIONS] [INPUT] Options: -o FILE --output=FILE output to file (default is standard output) -t --terse use terse output -- print only models -j --just-one find just one model -i --input-order use input order to select formulas -b INT --bound=INT set structure size bound (default 250) -l INT --limit=INT set step count limit (default 2000) -c --compact print structures compactly -s --sexpr print structures using S-expressions -m INT --margin=INT set output margin -q --quant read formulas using quantifier syntax -e --explicit print formulas using quantifier syntax -f --flatten print flattened formulas -p --proc-time print processor time in seconds -v --version print version number -h --help print this message

Syntax error messages produced by Chase include Emacs style file position information. When other error messages include position information, it points to the position of final period in the formula that caused the problem.

Terse output mode (`-t`

) is useful when Chase takes
many steps. When in this mode, Chase prints only models.

In input order mode (`-i`

) formulas are tried in the
order they are given in the input source file, otherwise, the
order is dynamically changed to prevent starvation of some
formulas.

Quantifier input syntax is enabled with `-q`

. In this
mode, quantifiers are explicit and a variable may be
uncapitalized. The keywords for universal quantification and
existential quantification are `forall`

and `exists`

respectively and used as in

forall x Y, P(x, Y) => exists z, Q(x, Y, c, z).

This sequent is translated into

P(X, Y) => Q(X, Y, c, Z).

S-expression output syntax is enabled with `-s`

. Each
structure is printed as an association list. This mode is useful
when another program consumes the output.

(struct (label 2) (parent 1) (sequent 1) (status model) (facts (assigned x y) (author x) (paper y) (read_score x y)))

The output of a run of Chase can be converted into an XHTML file that displays the tree of structures produced. The output for the conference management example above is approximately this.

(0)[]

One can click on a tree node to see its structure. Try it!

$ chasetree -h Usage: chasetree [OPTIONS] [INPUT] Options: -o FILE --output=FILE output to file (default is standard output) -r INT --ratio=INT set ratio between window heights (default 20%) -v --version print version number -h --help print this message

The file `chase.mk`

contains make rules for Chase.
This file is installed in the Chase `share`

directory.

A sample makefile that uses `chase.mk`

follows. If
you cut-and-paste from a browser window, be sure to convert the
leading spaces in the last line into a tab character.

include chase.mk TXTS := $(patsubst %.gl,%.txt,$(wildcard *.gl)) \ $(patsubst %.glx,%.txt,$(wildcard *.glx)) all: $(TXTS) clean: -rm $(TXTS)

The `m4`

macro processor can be used to include a
Geolog file into another Geolog file. To include the
file `foo.gli`

into `bar.glm`

type

m4_include(`foo.gli')m4_dnl

Process `bar.glm`

with

m4 -P bar.glm > bar.gl

The Makefile presented in previous section has an `m4`

rule for files with extension `.glm`

.

Models of theory `T` are found using an algorithm called
the
chase. The procedure starts with a structure in which each
constant in `T` is equated to itself. Queue `Q`
is created containing the initial structure, and the main loop
begins.

The chase for theory `T` repeats the following steps
until queue `Q` is empty.

- Take structure
`A`from`Q`. - If
`A`models`T`then output`A`. - Otherwise, choose a formula
`F`in`T`not satisfied by`A`.- Find a variable assignment
`S`for the universally quantified variables in`F`such that its antecedent is satisfied, but its consequent is not. - Apply
`S`to each disjunct in the consequent. - For each disjunct, substitute a freshly generated constant
for each existentially quantified variable, and add to the
queue a structure produced by augmenting
`A`with the disjunct. Mark`A`as being the parent of the new structure.

- Find a variable assignment

Daniel J. Dougherty of the Worcester Polytechnic Institute introduced me to geometric logic and minimization and provided guidance.