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

Chase User Guide

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₁, ..., a_n) in A implies P(h(a₁), ..., h(a_n)) in B.
For each n-place function f, f(a₁, ..., a_n) = a₀ in A implies f(h(a₁), ..., h(a_n)) = h(a₀) 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.

Input Syntax

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₁ & A₂ & ... & A_m => C₁ | C₂ | ... | 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 C_j is a conjunction of the form

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

Structures

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₁, ... , c_n)
f(c₁, ... , c_m) = c₀

where P and f are in the signature of T.

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

P(c₁, ... , c_n) in A implies c₁, ... , c_n in U
f(c₁, ... , c_m) = c₀ in A implies c₀, ... , c_m in 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.

Output Syntax

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

Formula Selection Order

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.

Usage

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)))

Output Visualization

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!

Usage

$ 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

Makefile

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)

Including Files

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.

Algorithm

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.
1. Find a variable assignment S for the universally quantified variables in F such that its antecedent is satisfied, but its consequent is not.
2. Apply S to each disjunct in the consequent.
3. 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.

Acknowledgment

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