CryptoPatrick / code

Code · Logic

Foras

A Rust port of the Otter 3.3 automated theorem prover.

Rust ~20,000 lines · 180 tests Active

What it is

Foras (First-Order ReASoner) is an automated theorem prover for first-order logic with equality. You give it axioms and the negation of a goal; it searches for a contradiction using resolution and paramodulation, and either prints a proof or reports that the search saturated without finding one.

It started as a small reasoner and became a faithful port of Otter 3.3, William McCune’s classic prover from Argonne National Laboratory. “Faithful” is measured, not claimed: a tool compares Foras’s search with C Otter’s clause by clause. On Otter’s 81 reference examples, 70 produce identical searches and the other 11 match up to the point where Otter’s memory accounting takes over.

Why

Language models are good at proposing proofs and bad at guaranteeing them. A prover is the opposite. Foras is the checking half of that pairing: a component an AI system can call to verify a logical claim, written in a language that’s easy to embed and deploy.

Using it

Foras reads Otter’s input format. A classic syllogism:

set(auto).

formula_list(usable).
all x (man(x) -> mortal(x)).
man(socrates).
-mortal(socrates).       % negated goal
end_of_list.

$ foras socrates.in
...
PROOF FOUND
  Given: 1
  Generated: 1
  Kept: 4

Useful options: --json prints the result, statistics and proof as JSON (for tools and agents), and --otter makes it behave exactly like C Otter 3.3f, quirks included.

Ideas for using it

  • Check an LLM’s logic. Let a model translate rules into clauses and let Foras decide whether they follow from each other. This is what my railcheck project does (write-up coming to the Lab).
  • An agent tool. Wrap --json behind an MCP server so an agent can ask “does this follow?” and get a proof back.
  • Teaching. Otter’s examples (group theory, the pigeonhole principle, puzzles) run unchanged, so Foras can be used to show how resolution works.
  • Regression oracle. Compare against another prover (Foras has been cross-checked against Z3 on 1,000 random problems with no disagreements).

Status

Under active development towards a 1.0 that accepts every Otter 3.3 input. Not yet published as a package.