ZENON-FORMAT(5)

💖 ZENON-FORMAT(5) 💖

okay bestie, welcome to the zenon-format manual page — it's a section 5 (that's "file formats", for the uninitiated 💅), and it's all about the Zenon format. come sit with me 🫶

---

✨ NAME ✨

zenon-format — an automated theorem prover for first-order classical logic, in format form. yes, the name is doing double duty, she contains multitudes 👑

---

🌸 DESCRIPTION 🌸

so Zenon (the icon, the legend) can eat a bunch of different input formats, and one of them is her very own, self-titled "Zenon" format. this page right here? it's the whole lore on that format. no gatekeeping 💖

🎀 the ground rules, bestie

• # and ; both start comments, and a comment runs all the way to the end of the line. everything after them is yapping and gets ignored 😌
• Identifiers start with A-Z, a-z, or an underscore. after that first character, they can keep going with 0 or more of: A-Z, a-z, 0-9, underscore, and the apostrophe. so yes, she can have a lil ' in her name, main character behaviour ✨
• Strings live inside double-quote characters. they may not contain the double-quote character, control characters, or any character beyond 126. hard limits, no negotiating 🚫
• Whitespace separates tokens, and that's genuinely it — otherwise it's ignored, it's just there for the vibe 💀

🦋 the syntax (this is the whole thing, don't skip)

file:
  | EOF
  | phrase file

phrase:
  | DEF "(" IDENT ident_list ")" expr
  | HYP int_opt hyp_name expr
  | GOAL expr
  | SIG IDENT "(" string_list ")" STRING
  | INDSET IDENT "(" ident_list ")"

expr:
  | IDENT
  | "(" IDENT expr_list ")"
  | "(" NOT expr ")"
  | "(" AND expr expr_list ")"
  | "(" OR expr expr_list ")"
  | "(" IMPLY expr expr_list ")"
  | "(" RIMPLY expr expr_list ")"
  | "(" EQUIV expr expr_list ")"
  | "(" TRUE ")"
  | TRUE
  | "(" FALSE ")"
  | FALSE
  | "(" ALL mlambda ")"
  | "(" EX mlambda ")"
  | mlambda
  | "(" TAU lambda ")"
  | "(" "=" expr expr ")"
  | "(" MATCH expr case_list ")"
  | "(" LET id_expr_list_expr ")"

expr_list:
  | expr expr_list
  | /* empty */

lambda:
  | "(" "(" IDENT STRING ")" expr ")"
  | "(" "(" IDENT ")" expr ")"

mlambda:
  | "(" "(" ident_list STRING ")" expr ")"
  | "(" "(" ident_list ")" expr ")"

ident_list:
  | /* empty */
  | IDENT ident_list

int_opt:
  | /* empty */
  | INT

hyp_name:
  | /* empty */
  | STRING

string_list:
  | /* empty */
  | STRING string_list

case_list:
  | /* empty */
  | "(" IDENT ident_list ")" expr case_list

id_expr_list_expr:
  | expr
  | IDENT expr id_expr_list_expr

💅 and now the token definitions, as promised

every one of these, exactly as she wrote them:

DEF "$def"
GOAL "$goal"
HYP "$hyp"
INDSET "$indset"
INDPROP "$indprop"
LET "$let"
MATCH "$match"
SIG "$sig"
NOT "-."
AND "/\"
OR "\/"
IMPLY "=>"
RIMPLY "<="
EQUIV "<=>"
TRUE "T."
FALSE "F."
ALL "A."
EX "E."
TAU "t."

not me needing you to notice that DEF is $def, GOAL is $goal, HYP is $hyp, INDSET is $indset, INDPROP is $indprop, LET is $let, MATCH is $match, and SIG is $sig — all the $-prefixed girlies. and the operators are living their best symbol lives: -., /\, \/, =>, <=, <=>. plus the truth-tellers T. and F., the quantifiers A. and E., and t. for TAU. iconic lineup, fr fr 🏆

---

🔥 SEE ALSO 🔥

• zenon(1) — go read her sister page, she's also that girl 💜

---

👑 AUTHOR 👑

this man page was written by David A. Wheeler. thank you for your service, king 🫶

---

📜 COPYRIGHT 📜

Zenon is released under the revised BSD license. this man page is released under both the revised BSD and MIT licenses — your choice, bestie, pick whichever one speaks to you 🎀

---

and that's the whole page!! mwah 💋 — written by David A. Wheeler, dated 2008-07, and yeah she's still ZENON-FORMAT(5) through and through. slay, stay proving theorems, bye!! 🌈✨