Tau Command-Line Interface User's Guide
TauTest Usage Synopsis
TauTest: TauTest [ option | file ] ...
Options:
-k Formulas Process Formulas instead of an input file
-d Display KB contents after parsing
-c FlexNormSpec Specify axiom-normalizing FlexNorm specification
(%u %c %v %q %n %a %f)
-C FlexNormSpec Specify definition-normalizing FlexNorm specification
(%u %c %v %q %n %a %f)
-n Show result of normalizing axioms in KB
-f FlexNormSet Specify test normalizations using a FlexNorm Set
-x NormalizerClass Name an extended normalizer class for FlexNorm
-a Run all tests (dump & normalize)
-p Use "pretty-printing" to display formulas
-P Don't use "pretty-printing" to display formulas (default)
-g grammar Specify the input grammar name ("KIF3" or "KIF3if")
-l Interpret KIF "logical constants" as predicate formulas
-L Prohibit KIF "logical constants" (default)
-N Read KIF (/= ...) as (not (= ...))
-X Dissect KB formulas
--ah Display the Arithmetical Hierarchy values of each KB formula
--bt Apply the Brand Transformations to the axioms in the KB
--bt=[FSTGKR] Apply the specified Brand Transformations to the axioms in the KB
F/f Flattening
S/s Symmetry
T/t Transitivity
--ap Apply anti-prenexing to axioms in the KB
--dp Apply the Davis-Putnam method to axioms in the KB
--idp Apply the incremental Davis-Putnam method to successive KB axioms
--rt Submit each axiom to the Refutation Tree individually
--RT Submit all axioms to the Refutation Tree collectively
-E Use the K&M Proof Procedure with identity
--DF Use the K&M Proof Procedure with identity--depth-first strategy
--SP Use "strategy" prover
--id=identifier Specify the identifier available in templates and their output names
--ftl=FMTemplate Display the proof using the specified FreeMarker template
--filter=actions Control which proof actions are recorded for template rendering
--tdata=name=value Add directly to the template data model
-v Formulas Record conclusions to prove
-V Formulas Submit the specified formulas as conclusions to the selected prover
-e Formulas Record formulas for equality test
-r Formulas Record formulas for comparison test
-o Formulas Record formulas for occurs test
-s Formulas Record formulas for subformula sort test
-S Formulas Record formulas for subformula simplification test
-t Formulas Record formulas for variable substitution test
-T Var_Subs Record variable substitutions
--Pclass Sort premises by their formula class: QFF -> EQF -> UQF
--Prank Sort premises by their Arithmetical Hierarchy linear rank
--Pfull Sort premises by class then by AH index
--Pnone Don't sort premises (default)
--MI=cycleMax Specify the maximum number of instantiation cycles in the proof
--ML=ecMax Specify the maximum number of lines in the Elimination Column
--MT=timeMax Specify the maximum time to spend attempting a proof
--MC=cpuMax Specify the maximum CPU time to spend attempting a proof
--cfg=configDesc Specify an alternate configuration name
--config=configDesc Specify an alternate configuration name
--showCfg Display the currently active configuration
--showConfig Display the currently active configuration
--dumpCfg Dump the entire configuration database
--dumpConfig Dump the entire configuration database
-? --help Print this help message
--flexNorm Show help on FlexNormSpec and FlexNormSet
--ptraceCodes Show help on "--ptrace" options
--debug Enable debugging output and every trace channel
--echo Echo the following argument
--PPintro=string Specify pretty-printer intro string
--PPprefix=string Specify pretty-printer per-line prefix string
--PPindent=string Specify pretty-printer indent string
--PPtail=string Specify pretty-printer tail string
--ptrace=enables Select trace channels (hexadecimal)
--ptrace Enable all non-debug trace channels
-A Arg_File Read arguments from the specified Arg_File
FlexNorm Control Strings
FlexNorm Set: Semicolon-separated sequence of FlexNorm Specs
FlexNorm Spec: Concatenation of FlexNorm Operators
FlexNorm Operators:
Normal Form Operators:
^n NNF: Negation Normal Form ("%m %n")
^p PNF: Prenex Normal Form ("%m %n %u %v %q")
^s SNF: Skolem Normal Form ("%m %n %u %v %q %s")
^S SNF keeping universal quantifiers ("%m %n %u %v %q %S")
^c CNF: Conjunctive Normal Form ("%m %n %u %v %q %s %a %f")
^C CNF keeping universal quantifiers ("%m %n %u %v %q %S %a %f")
^d DNF: Disjunctive Normal Form ("%m %n %u %v %q %s %o %f")
^D DNF keeping universal quantifiers ("%m %n %u %v %q %S %o %f")
^N Default Normalization
Transformation Primitive Operators:
%m Material Implication and Equivalence Removal
%e Split Material Equivalences and Exclusive ORs
%c Standardize Binary Connectives (replace them with ANDs, ORs or NOTs)
%n Negation Minimization
%u Sentential Form (add universal quantifiers for free variables)
%v Separate Variables ("rename apart")
%q Segregate Quantifiers (at front of formula)
%Q Minimize Quantifier scopes
%s Skolemize (replace existentials with Skolem functions)
%S Skolemize retaining universal quantifiers
%a Distribute AND Over OR
%o Distribute OR Over AND
%f Flatten nested commutative / associative connectives
%r Sort (_r_eorder) commutative / associative connectives
%R Simplify (_R_educe) redundant, adjacent subformulas
%t Thomas' stage IV simplifications
Non-Equivalence-Preserving Operators:
*n Add negation
*d Form the dual
Extended (User-supplied) Normalizers (see the "-x" option):
%0 First extended normalizer
%1 Second extended normalizer
...
%9 Last extended normalizer
Proof Tracing Control Codes
Proof tracing channel enable bits:
ECPut 0001
ECDup 0002
ECTake 0004
NewVar 0008
EI 0010
UI 0020
NewFreeTerm 0040
R3NFTerm 0080
ProofDone 0100
CycleOverflow 0200
ECOverflow 0400
CPULimit 0800
ClockLimit 1000
Proved 2000
Unproved 4000
Disproved 8000
debug 10000