Prover9 Manual Version 2009-02A

Interpformat

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

The transformations are listed here.

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:

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