Automated theorem prover for first-order classical logic

Zenon is an automated theorem prover for first order classical logic

with equality, based on the tableau method. Zenon can read input files

in TPTP, Coq, Focal, and its own Zenon format. Zenon can directly

generate Coq proofs (proof scripts or proof terms), which can be

reinserted into Coq specifications. Zenon can also be extended.

Command | Description |
---|---|

zenon | Automated theorem prover for first-order classical logic |

File | Description |
---|---|

zenon-format | Automated theorem prover for first-order classical logic format |