Skip to main content

prover9.org

Prover9

Prover9 Manual

Introduction What's New Installation Running Prover9 Input Files Clauses & Formulas

TPTP

TPTP Mode SInE Premise Selection Strategy Scheduling Proof Verification

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 Checkpoint and Resume

Mace4

Introduction Input TPTP Mode Checkpoint and Resume Options Arithmetic Interpformat Isofilter

Related Programs

Prooftrans FOF-Prover9 More Programs

Reference

Command-Line Reference All Prover9 Options Advanced Build Modes Glossary References Privacy Policy

← 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

Next Section: Checkpoint and Resume

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