The project
The full story.
What it is, why it exists, how to use it and where it stands.
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 a classic resolution prover written in C. “Faithful” is measured, not claimed: a tool compares Foras’s search with the C original’s clause by clause. On the original’s 81 reference examples, 70 produce identical searches and the other 11 match up to the point where the original’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 the classic prover’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 a compatibility flag makes it behave exactly like the C original, 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: Generate, but verify.
- An agent tool. Wrap
--jsonbehind an MCP server so an agent can ask “does this follow?” and get a proof back. - Teaching. The classic reference 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 input the C original accepts. Not yet published as a package.
