Interpformat

The models (structures) in Mace4 output files can be transformed in various ways with the program Interpformat.

The transformations are listed here.

standard: This transformation simply extracts the structure from the file and reprints it in the same (standard) format, with one line for each operation. The result should be acceptable to any of the LADR programs that take standard structures.
standard2: This is similar to standard, except that the binary operations are split across multiple lines to make them more human-readable. The result should be acceptable to any of the LADR programs that take standard structures.
portable: This form is list of ... of lists of strings and natural numbers. It can be parsed by seveal scripting systems such as GAP, Python, and Javascript. See the section Portable Format.
tabular: This form is designed to be easily readable by humans. It is not meant for input to other programs.
raw: This form is a sequence of natural numbers.
cooked: This form is a sequence of ground terms.
xml: This is an XML form. Here is a DTD for LADR interpretations, and here is an XML stylesheet for transforming the XML to HTML.
tex: This generates LaTeX source for the interpretation.

Examples

The following Mace4 job creates an output file containing one model in "standard" (the default) format.

mace4 -c -f x2.in > x2.mace4.out

The following Interpformat jobs take the Mace4 output file, extract the model, and transform it as described above.

interpformat standard  -f x2.mace4.out > x2.standard
interpformat standard2 -f x2.mace4.out > x2.standard2
interpformat portable  -f x2.mace4.out > x2.portable
interpformat tabular   -f x2.mace4.out > x2.tabular
interpformat raw       -f x2.mace4.out > x2.raw
interpformat cooked    -f x2.mace4.out > x2.cooked
interpformat xml       -f x2.mace4.out > x2.xml
interpformat tex       -f x2.mace4.out > x2.tex

Portable Format

The portable format for interpretations can be parsed by several scriping languages including Python and GAP. Here is a counterexample on ternary relations in lattice theory. The result contains one interpretation of size 4 containing two binary functions (meet and join), one binary relation (less-or-equal), two ternary relations, and three constants.

mace4 -c -f LT-port.in | interpformat portable > LT-port.out

The result is a list of interpretations:

each interpretation is a triple: [size-of-interpretation (say n), comments, list-of-operations];
each operation is a 4-tuple: ["function" | "relation", name-of-operation, arity, values];
values of operations (domain elememts are [0 ... n-1]):
- constant (nullary function): domain element;
- unary function: list of domain elements;
- binary funcion: 2-dimensional list (list of lists) of domain elements;
- ternary funcion: 3-dimensional list of domain elements;
- etc.
- relations are similar but with values of 0 (FALSE) or 1 (TRUE).

Here is a simple Python script that reads a list of portable interpretations and prints them in a different form.

port.py < LT-port.out > LT-port.out2

Here is a simple GAP session that reads and prints a list of portable interpretations.

% gap -b
GAP4, Version: 4.4.7 of 17-Mar-2006, i486-pc-linux-gnu-i486-linux-gnu-gcc
gap> interpretations := EvalString(StringFile("LT-port.out"));;
gap> interpretations;
[ [ 4, [ "=(number,1)", "=(seconds,0)" ], 
      [ [ "relation", "<=", 2, [ [ 1, 1, 1, 1 ], [ 0, 1, 0, 0 ], 
                  [ 0, 1, 1, 0 ], [ 0, 1, 0, 1 ] ] ], 
          [ "function", "^", 2, [ [ 0, 0, 0, 0 ], [ 0, 1, 2, 3 ], 
                  [ 0, 2, 2, 0 ], [ 0, 3, 0, 3 ] ] ], 
          [ "function", "v", 2, [ [ 0, 1, 2, 3 ], [ 1, 1, 1, 1 ], 
                  [ 2, 1, 2, 1 ], [ 3, 1, 1, 3 ] ] ], 
          [ "function", "c1", 0, 2 ], [ "function", "c2", 0, 0 ], 
          [ "function", "c3", 0, 3 ], 
          [ "relation", "A", 3, [ [ [ 1, 1, 1, 1 ], [ 0, 1, 0, 0 ], 
                      [ 0, 1, 1, 0 ], [ 0, 1, 0, 1 ] ], 
                  [ [ 1, 0, 0, 0 ], [ 1, 1, 1, 1 ], [ 1, 0, 1, 0 ], 
                      [ 1, 0, 0, 1 ] ], 
                  [ [ 1, 0, 0, 0 ], [ 0, 1, 0, 0 ], [ 1, 1, 1, 0 ], 
                      [ 0, 0, 0, 0 ] ], 
                  [ [ 1, 0, 0, 0 ], [ 0, 1, 0, 0 ], [ 0, 0, 0, 0 ], 
                      [ 1, 1, 0, 1 ] ] ] ], 
          [ "relation", "B", 3, [ [ [ 1, 1, 1, 1 ], [ 0, 1, 0, 0 ], 
                      [ 0, 1, 1, 0 ], [ 0, 1, 0, 1 ] ], 
                  [ [ 1, 0, 0, 0 ], [ 1, 1, 1, 1 ], [ 1, 0, 1, 0 ], 
                      [ 1, 0, 0, 1 ] ], 
                  [ [ 1, 0, 0, 1 ], [ 0, 1, 0, 1 ], [ 1, 1, 1, 1 ], 
                      [ 0, 0, 0, 1 ] ], 
                  [ [ 1, 0, 1, 0 ], [ 0, 1, 1, 0 ], [ 0, 0, 1, 0 ], 
                      [ 1, 1, 1, 1 ] ] ] ] ] ] ]
gap>

Next Section: Isofilter