prove_session
Prove the conclusion from premises in the active session using a theorem prover like Vampire, E, or Prover9.
Instructions
Execute a proof using the current session's premises and conclusion.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| prover | No | Which theorem prover to use (simple is built-in, others require installation) | vampire |
| session | No | Session name (defaults to current session) |