Skip to main content

prover9.org

Prover9

Prover9 Manual

Introduction Installation Running Prover9 Input Files TPTP Mode Clauses & Formulas

Search Prep

Auto Modes Term Ordering More Prep Search Limits

Inference

The Loop Select Given Inference Rules Process Inferred

Output

Output Files

More Features

Weighting Attributes Goals and Denials Hints Production Mode Advanced Features

Mace4

Introduction Input TPTP Mode Options Arithmetic Interpformat Isofilter

Related Programs

Prooftrans FOF-Prover9 More Programs

Reference

All Prover9 Options Glossary References

← prover9.org

Built on LADR by
William McCune (1953–2011)
Maintained by
prover9.org

prover9.org / Manual / Advanced Features

Advanced Features

Actions
Hints
Semantics
Clause Properties
Keep and Delete Rules
Given Selection

prover9.org · LADR-2026 project
Prover9/Mace4 by William McCune (1953–2011), Argonne National Laboratory. The original algorithms, strategies, and core logic of the LADR library remain McCune's work.

License (GPLv2) · GitHub