Other LADR Prograns

The page describes several other programs that have constructed with the same code base (LADR) as Prover9, Prooftrans, Mace4, and Interpformat.

When we write that a program takes a "stream" of objects, we mean that it reads them from the standard input, and the objects are not enclosed in objects(..) and end_of_list.

When we write that a program takes a "set" of objects, we mean that the filename containing the objects is an argument to the program, and the objects are not enclosed in objects(..) and end_of_list.

When we write that a program takes a "list" of objects, we mean that the filename containing the objects is an argument to the program, and the objects are enclosed in objects(..) and end_of_list.

Contents

Clausefilter -- filter clauses with models
Clausetester -- check clauses in models
Interpfilter -- filter models with clauses
Isofilter -- remove isomorphic models
Rewriter -- demodulate terms

Clausefilter

Given a set of interpretations, a test to perform, and a stream of clauses, this program outputs the clauses that pass the test.

The accepted tests are true_in_all, true_in_some, false_in_all, and false_in_some.

Example: given a set of non-modular orthomodular lattices and a stream of identities, print the identities that are false in all of the lattices. This job was used when searching for modular ortholattice (MOL) single axioms: any MOL single axiom is false in all non MOLs.

clausefilter non-MOL-OML.interps false_in_all < MOL-cand.296 > MOL-cand.238

Clausetester

This program takes a set of interpretations and stream of clauses. For each clause, the interpretations in which the clause is true are shown, and at the end the number of clauses true in each interpretation is shown.

Example:

clausetester uc-18.interps < uc-hunt.clauses > uc-hunt.out

Interpfilter

Given a set of clauses, a test to perform, and a stream of interpretations, this program outputs the interpretations that pass the test.

The accepted tests are all_true, some_true, all_false, and some_false.

Example:

Isofilter

Given a stream of interpretations, remove the isomorphic ones.

Example:

mace4 -N6 -m -1 -f BA2.in | get_interps > BA2.interps 
isofilter < BA2.interps > BA2.interps2

Note that the two models in BA2.interps2 differ only in one of the constants. In this case the constants come from existentially quantified variables in the goal, and all we really care about is the lattice. We can tell Isofilter to ignore differences in constants by giving it the argument ignore_constants as in the following command.

isofilter ignore_constants < BA2.interps > BA2.interps3

The output of isofilter is frequently used as input to a program that expects the interpretations to be in a list of interpretations; we can tell isofilter to put the output in that form by giving it the argument wrap as in the following command.

isofilter ignore_constants wrap < BA2.interps > BA2.interps4

Finally, we can string together some of the preceding commands as follows.

mace4 -N6 -m -1 -f BA2.in | get_interps | isofilter ignore_constants wrap > BA2.interps5

Rewriter

Rewrite a stream of terms with a list of demodulators. The demodulators are used left-to-right as given, and they are not checked for termination.

Basic example that canonicalizes group expressions:

rewriter group.demods < group-terms.in > group-terms.out

This example canonicalizes Boolean ring expressions. It uses associative-commutative (AC) operations and the op command to change the parsing rules.

rewriter bool-ring.demods < bool-ring.in > bool-ring.out

This example rewrites identities in terms of {meet,join,complementation} into the Sheffer stroke.

rewriter BA-Sheffer.demods < BA4.in > BA4.out

Next Section: All Options