SCHEMA USERS GUIDE

henry.kautz@gmail.com

Schema is a language for specifying propositional logic theories using a first-order logic-like syntax. The Schema interpreter produces propositional CNF (conjunctive normal form) which can be input to any satisfiability testing program.

The Schema interpreter is written in Common Lisp, but it is not necessary to know how to program in Lisp in order to use Schema.

Using Schema

Invoke any implementation of Common Lisp, and load the file "schema.el". The following Lisp functions are available:

(parse '(SCHEMA ...) '(OBSERVATION ...))
Parse a list of schemas (see BNF syntax below) and return a list of clauses in symbolic form. Each OBSERVATION is a ground atom that is asserted to be true. When the schemas are expanded, they are simplified by replacing observed atoms by 1 (true) and all non-observed atoms that employ the same predicates by 0 (false).

(instantiate "test.wff" "test.scnf" &optional "test.obs")
Reads the Schema file "test.wff", instantiates it, and saves the result in symbolic conjunctive normal form in the file "test.scnf". The optional file "test.obs" contains a sequence of observed ground atoms.

(propositionalize "test.scnf" "test.cnf" "test.map")
Reads the symbolic conjunctive normal form file "test.scnf" and creates a DIMACS format CNF file3 "test.cnf". In DIMACS format (the standard input language for all modern SAT solvers), propositions are represented by positive and negative integers. The mapping from symbolic ground atoms to integers is written to the file "test.map". The file "test.cnf" may then be sent to a SAT solver, such as Minisat or walksat. Suppose the file "test.soln" specifies a solution satisfying assignment, specified by a sequence of positive and negative integers. (If for some integer, neither the integer nor its complement appears, then it is assumed to be false (negative) for the assignment.)

(interpret "test.soln" "test.map" "test.out") Reads in a DIMACS solution file "test.soln" of the format specified above and a mapping file "test.map", and creates a file "test.out" containing the positive literals in the satisfying assignment in symbolic form.

Language

A Schema program consists of a sequence of options, type declarations, and formulas. Options control certain details of the intrepreter. Type declarations bind type names to sets of Herbrand terms. Formulas are composed, as in first-order logic, of predicates, variables, constants, function symbols, logical connections, and quantifiers. The basic function of the Schema interpreter is to instantiate the variables in each formula and convert the result to CNF.

Formulas are specified in prefix (LISP) notation. The quantifiers, all and exists, iterate over sets of Herbrand terms. Terms are integers, constants, or complex terms built using uninterpreted function symbols. A quantified formula is represented by a list containing the quantifier, a variable, a set of terms, a test (integer) expression, and the subformula to which the quantification is applied. The subformula is instantiated only for bindings of the variable for which the test is true (not equal to 0). For example,

(all x (range 1 10) (= 0 (mod x 2)) (p x))

can be read, "for all x in the range 1 through 10, such that x is even, assert (p x)".

Propositions are expressed in Schema as either atomic symbols or complex propositions specified by a list beginning with a predicate followed by zero or more terms. Terms can be built from interpreted functions such as + and uninterpreted function symbols. For example, the literal expression (winner john (round (* 3 8))) is instantiated as

(winner john (round 24))

where "winner" is a predicate, "john" is a simple term, "round" is an uninterpreted function symbol, and "(round 24)" is a complex term.

The integer values 0 and 1 are used to represent false and true respectively in intger expressions. Integer expressions may include arithmetic functions (+, -, *, div, rem, mod), comparison functions (<, <=, =, >=, >, member), set composition functions (enumeration lists, union, intersection, setdiff), logical functions (and, or, not), and observed predicates. Non-observed predicates may not appear in an integer expression. Note that logical functions in integer expressions are evaluated by the Schema interpreter and do not appear in the final CNF, unlike the logical operators that have the same names.

Schema BNF

<schema> = <option> | <type declaration> | <formula>

<option> = (option <option name> <integer expression>)

<option name> = compact | shadow

<type declaration> = (type <type name> <set expression>)

<formula> = <proposition> | (not <formula>) | (and <formula>*) | (or <formula>*) | (implies <formula> <formula>) | (equiv <formula> <formula>) | (all <variable> <set expression> <integer expression> <formula>) | (exists <variable> <set expression> <integer expression> <formula>) | (if <integer expression> <formula>)

<proposition> = <predicate symbol> | (<predicate symbol> <term>*)

<set expression> = <type name> | (set <term> <term>*) | (range <integer expression> <integer expression>) | (union <set expression> <set expression>) | (intersection <set expression> <set expression>) | (setdiff <set expression> <set expression>) | (lisp <lisp list valued expression>)

<term> = <constant symbol> | <integer expression> | <variable> | (<uninterpreted function symbol> <term>*)

<integer expression> = <number> | <variable> | (<observed predicate symbol> <term>*) | (member <term> <set expression>) | (not <integer expression>) | (and <integer expression>*) | (or <integer expression>*) | (<operator> <integer expression> <integer expression>) | (lisp <lisp integer valued expression>)

<operator> = + | - | * | div | rem | mod | < | <= | > | >= | = | eq | neq | ** | bit

Options

(option compact-encoding 1) ; Allow new propositions to be created to reduce the size of the instantiated formula, as described below (default).

(option compact-encoding 0) ; Do not create new propositions.

(option shadow 0) ; Do not allow the same variable name to be used in nested subformulas (default).

(option shadow 1) ; Allow an inner quantified variable to shadow an outer variable of the same name.

Compact Encodings

The input formulas need not be in conjunctive normal form. Converting a formula to CNF using only the user-defined propositions can cause its size to increase exponentially. By creating new propositions, the Schema interpreter can guarantee the output formula is linear in the size of the instantiated input formula. Where

M = number of input formulas L = length of the longest input formula D = size of the largest set appearing in a quantification statement N = deepest nesting of quantifiers in a formula the size of the output CNF is O(M*L*D^N)

When new propositions are introduced in this manner, the relationship between the input and output formulas is:

1. The output formula entails the input formula; and 2. Any model of the input formula can be extended to a model of the output formula.

Condition 1 can also be expressed as:

1'. Any model of the output formula is also a model of the input formula.

When no new propositions are introduced, the input and output formulas are equivalent.