Clinical eligibility criteria express numerical comparisons and Boolean relations in prose. We translate them into executable typed formulas using a neural parser, grammar and ontology constraints, and an independent symbolic verifier. The formulas have precise semantics, source-linked predicates, and an auditable record of type, unit, grounding, and consistency checks. On 200 independently double- annotated criteria, a development-selected threshold yields 89.2% logical correctness at 78.5% coverage. At a matched 78% coverage, neuro-symbolic, neural, and rule selection achieve 89.7%, 88.5%, and 85.3% correctness, respectively. We evaluate these trade-offs with exact logical equivalence, confidence intervals, and full risk–coverage curves. Structural breakdowns, candidate oracles, augmentation experiments, and controlled edits across two backbones identify Boolean scope and omitted predicates as the main remaining errors. The symbolic interface makes these failures inspectable while separating formal validity from semantic correctness. The study provides an executable approach to quantitative semantic parsing and a controlled testbed for diagnosing its compositional bottlenecks.