Automated theorem proving
Explore first-order logic with iProver
Write a TPTP or Prover9 problem, run iProver, and inspect its result and proof.
Create a first-order problem
Write a problem or load an example to begin.
Editor below is live. Change the formula, check its syntax, then run iProver to see the result. Cut and paste your own formulas and run iProver!
Load an example
Problem editor
Execution
Project statistics
Run statistics
Loading...- iProver runs
- -
- Avg iProver time
- -
- Unsat
- -
- Sat
- -
- Unknown
- -
- Timeouts
- -
- LLM calls
- -
- Avg LLM time
- -