Automated theorem proving
Explore first-order logic with iProver
Write a TPTP problem, run iProver, and inspect its result and proof.
Create a FOF 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
Execution
Project statistics
Run statistics
Loading...- iProver runs
- -
- Avg iProver time
- -
- Unsat
- -
- Sat
- -
- Unknown
- -
- Timeouts
- -
- LLM calls
- -
- Avg LLM time
- -