prove
Verify logical conclusions from premises using resolution-based theorem proving. Input premises and conclusion to determine if the statement follows logically.
Instructions
Prove a logical statement using resolution.
When to use: You have premises and want to verify a conclusion follows logically. When NOT to use: You want to find counterexamples (use find-counterexample instead).
Example: premises: ["all x (man(x) -> mortal(x))", "man(socrates)"] conclusion: "mortal(socrates)" → Returns: { success: true, result: "proved" }
Common issues:
"No proof found" often means inference limit reached, not that the theorem is false
Try increasing inference_limit for complex proofs
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| premises | Yes | List of logical premises in FOL syntax | |
| conclusion | Yes | Statement to prove | |
| inference_limit | No | Max inference steps before giving up (default: 1000). Increase for complex proofs. | |
| enable_arithmetic | No | Enable arithmetic predicates (lt, gt, plus, minus, times, etc.). Default: false. | |
| enable_equality | No | Auto-inject equality axioms (reflexivity, symmetry, transitivity, congruence). Default: false. | |
| engine | No | Reasoning engine: 'prolog' (Horn clauses), 'sat' (general FOL), 'auto' (select based on formula). Default: 'auto'. | |
| verbosity | No | Response verbosity: 'minimal' (token-efficient), 'standard' (default), 'detailed' (debug info) |