Prover9 Manual Version 2009-02A

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

Given a set of interpretations, a test to perform, and a stream of formulas, this program outputs the formulas that pass the test. (If non-clausal formulas with free variables are given, their universal closures are used and output.)

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 formulas. For each formula, the interpretations in which the formula is true are shown, and at the end the number of formulas true in each interpretation is shown. (If non-clausal formulas with free variables are given, their universal closures are used and output.)

Example: 

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

Interpfilter

Given a set of formulas, a test to perform, and a stream of interpretations, this program outputs the interpretations that pass the test. (If non-clausal formulas with free variables are given, their universal closures are used.)

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

Example: from a list of quasigroups, extract the associative-commutaive ones. 

interpfilter assoc-comm.clauses all_true < qg4.interps > qg4-ac.interps

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

TPTP Translators

The TPTP Problem Library contains thousands of problems for theorem provers, and the TPTP Language is widely used in the community. LADR has two programs to translate between the LADR and TPTP languages. These programs are new and experimenal, and they do not support all of the language features.

TPTP_to_LADR

This program takes a TPTP problem file and produces a bare input file suitable for input to Prover9 or Mace4. For example, 
tptp_to_ladr < PUZ031-1.tptp > PUZ031-1.in
prover9 -f PUZ031-1.in > PUZ031-1.out
If you prefer, those two processes can be piped together: 
tptp_to_ladr < PUZ031-1.tptp | prover9 > PUZ031-1.out2
Some of the TPTP language features that are not yet supported are comment blocks, system comments, real numbers, natural numbers as distinct objects, and distinct objects with double quotes.

Some future version of LADR will likely support direct input of TPTP files to Prover9 and Mace4, without having to invoke a translator.

LADR_to_TPTP

This program takes a Prover9 input file and produces a TPTP problem file. A difficulty with this kind of translation is that TPTP accepts a more restriced class of function and predicate symbols. When the translator sees symbols that are not accepted by TPTP, it introduces new symbols, and it gives the symbol mapping as comments in the output. Ordinary TPTP constant, function, and predicate symbols must start with lower case a-z, and any remaining characters must be alphanumeric or _ (underscore). That is, they must match the (Unix-style) regular expression "[a-z][a-zA-Z0-9_]*".

Here is an example that contains several unacceptable symbols. 

ladr_to_tptp < RBA-2.in > RBA-2.tptp
Instead of introducing new symbols such as tptp0, you can tell ladr_to_tptp to put single quotes around unacceptable symbols by using the command-line option -q. See the following example. 
ladr_to_tptp -q < RBA-2.in > RBA-2q.tptp
Next Section: All Options