Module formula 

A self-contained parser from formal first-order-logic surface text to ProofExpr.

The natural-language front end (logicaffeine_language) is excellent at English — unary predicates, simple binary relations from transitive verbs — but a geometry axiom base needs formal relations of higher arity (Cong(a,b,c,d), Bet(a,b,c)) and explicit quantifier prefixes that no English sentence expresses. This module is the seam: a small recursive-descent parser, deliberately independent of the 12k-line NL parser (the same self-containment that tactic_script has), turning a line like

for all a b c d e f, if Cong(a, b, c, d) and Cong(a, b, e, f) then Cong(c, d, e, f)

directly into the ProofExpr the prover and the multi-theorem driver already consume. It is the surface for ## Axiom / ## Theory (the seam for Tarski).

Conventions

• An identifier that leads with an uppercase letter or a digit is a CONSTANT (ProofTerm::Constant) — a fixed point like P, Q, A; one that leads with a lowercase letter is a VARIABLE (ProofTerm::Variable) — a bound point like a, b. This matches the verifier’s standard FOL reading (a lowercase-leading symbol is a variable).
• Connectives, lowest precedence first: quantifiers (for all, there exists) < iff < implication (if … then …, implies, ->) < or < and < not < atoms. Implication is right-associative.
• Both an English-flavoured spelling and a symbolic one are accepted: and/∧, or/∨, not/¬, implies/->/→, iff/<->/↔, for all/forall/∀, there exists/exists/∃.

Structs

FormulaError

A failure to parse formal-logic surface text.

Functions

parse_formula

Parse formal first-order-logic surface text into a ProofExpr.