LADR Software Update

Prover9

• A Manual!
• Automatic Modes
• Selection of the Given Clause
• Semantic Guidance
• Goals and Denials
• Hints
• Term Ordering
• Weighting
• Attributes
• Actions
• Output Files
• FOF Reduction
• Prooftrans

Mace4

• Compatibility with Prover9 Inputs
• Interpformat

Other LADR Programs