ZENON(1)

💖 ZENON(1) — like, the manual page for zenon, bestie 💖

okay so picture this: it's ZENON(1), a User Commands page, and it's here to tell you about zenon, the automated theorem prover that is genuinely the moment. pull up a chair, grab a strawberry 🍓, and let's get into it.

---

✨ NAME ✨

zenon — automated theorem prover for first-order classical logic. no cap, that's literally the whole vibe. 💅

---

🌸 SYNOPSIS 🌸

zenon [OPTIONS] FILE

that's it. that's the whole summoning ritual. options first, then your file, slay. 🎀

---

🦋 DESCRIPTION 🦋

okay so Zenon is an automated theorem prover for first order classical logic with equality, based on the tableau method. it's giving rigorous. it's giving methodical. 🔥

here's the tea on what it can read — Zenon can read input files in:

• TPTP
• Coq
• Focal
• and its own Zenon format 👑

and it doesn't just read — Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted into Coq specifications. reinserted!! into the specs!! iconic behavior fr fr. 💖

also it can be extended, so go off, customize it, make it yours. ✨

---

💅 OPTIONS 💅

first things first, and this is important: if file is -, it will read input from stdin. yes, the dash. the classic. the icon. 🫶

• -context — provide context for checking the proof independently
• -d — debug mode 🐛
• -errmsg <message> — prefix warnings and errors with <message>
• -help, --help — print this option list and exit
• -I <dir> — add <dir> to the include path (for TPTP input format)
• -icoq — read input file in Coq format
• -ifocal — read input file in Focal format
• -itptp — read input file in TPTP format
• -iz — read input file in Zenon format (default) — this is the home-team default 💜
• -loadpath — path to Zenon's coq libraries (default /usr/share/zenon)
• -max <s>[kMGT]/<i>[kMGT]/<t>[smhd] — set size, step, and time limits ⏱️
• -max-size <s>[kMGT] — limit heap size to <s> kilo/mega/giga/tera word (default 100M)
• -max-step <i>[kMGT] — limit number of steps to <s> kilo/mega/giga/tera (default 10k)
• -max-time <t>[smhd] — limit CPU time to <t> second/minute/hour/day (default 5m)
• -ocoq — print the proof in Coq script format
• -ocoqterm — print the proof in Coq term format
• -oh <n> — print the proof in high-level format up to depth <n>
• -ol — print the proof in low-level format
• -olx — print the proof in raw low-level format
• -om — print the proof in middle-level format
• -onone — do not print the proof (default)
• -opt0 — do not optimise the proof
• -opt1 — do peephole optimisation of the proof (default) 👀
• -p0 — turn off progress bar and progress messages
• -p1 — display progress bar (default)
• -p2 — display progress messages
• -q — (quiet) suppress proof-found/no-proof/begin-proof/end-proof 🤫
• -rename — prefix all input symbols to avoid clashes
• -rnd <seed> — randomize proof search 🎲
• -stats — print statistics 📊
• -short — output a less detailed proof
• -v — print version string and exit
• -versions — print CVS version strings and exit
• -w — suppress warnings
• -where — print the location of the zenon library and exit
• -wout <file> — output errors and warnings to <file> instead of stderr
• -x <ext> — activate extension <ext>

---

🌈 EXAMPLE 🌈

okay bestie, here's the whole thing in action. the command:

zenon -itptp -ocoq /usr/share/zenon*/examples/tptp-COM003+2.p

will take the input file "tptp-COM003+2.p" in TPTP format (-itptp), search for a proof, and produce any proof output in Coq format (-ocoq). the way that tptp-COM003+2.p is literally a TPTP representation of the halting problem 😭 and Zenon can prove this. it can prove the halting problem representation. main character energy fr fr. 👑

and it will print out:

(* PROOF-FOUND *)
(* BEGIN-PROOF *)
... details of proof in Coq format
(* END-PROOF *)

(* PROOF-FOUND *) — the moment. the reveal. the slay. ✨

---

🧚 SEE ALSO 🧚

zenon-format(5) — go read it, it's the companion piece, iykyk 💜

---

🎀 AUTHOR 🎀

This man page was written by David A. Wheeler. thank you for your service 🫶

---

👑 COPYRIGHT 👑

Zenon is released under the revised BSD license. This man page is released under both the revised BSD and MIT licenses (your choice). pick your fighter, both are valid. 💖

---

and that's the whole page, bestie!! this was David A. Wheeler's work from 2008-07, and it's the ZENON(1) page from the User Commands corner of the manual, so go forth and prove some theorems. literally obsessed with you for reading all the way down here. 🌸💅✨