medovina/natty

---

medovina/natty.json

{
  "createdAt": "2024-02-18T09:21:54Z",
  "defaultBranch": "main",
  "description": "Natty is a natural-language proof assistant with an embedded automatic prover for higher-order logic.  It is in an early stage of development.",
  "fullName": "medovina/natty",
  "homepage": "",
  "language": "OCaml",
  "name": "natty",
  "pushedAt": "2025-11-26T17:26:16Z",
  "stargazersCount": 38,
  "topics": [],
  "updatedAt": "2025-11-26T17:26:20Z",
  "url": "https://github.com/medovina/natty"
}

Natty

Natty is a natural-language proof assistant with an embedded automatic prover for higher-order logic. It can read input containing axioms, definitions, and theorems written in natural language with a restricted vocabulary and grammer. Any theorem in the input may optionally include a proof, also written in natural language. Natty translates the input into a series of statements of higher-order logic, and attempts to prove the input theorems automatically.

Natty’s automatic prover is based on a subset of the higher-order superposition calculus[^1].

Natty is in an early stage of development, and is currently only able to prove some basic theorems about the natural numbers and integers. As such, in its present form it will probably be of interest only to theorem proving researchers and enthusiasts.

Prerequsities

Natty is written in OCaml, using Dune as its build system. It requires OCaml version 5.4 and depends on several OCaml libraries: MParser, psq, and yojson. You can install these libraries using opam:

$ opam install mparser mparser-re psq yojson

Running Natty

You can invoke Natty on an input file directly:

$ ./natty math/nat.n

By default, Natty will attempt to prove theorems only in the module (e.g. nat.n) that you have specified. The -r option asks Natty to also prove theorems in all modules that the given module uses (recursively).

The -p option asks Natty to output a proof of each theorem that it proves:

$ ./natty -p math/nat.n

The -d option will print verbose debug output, showing all inferences that Natty makes as it searches for proofs.

By default, Natty will stop as soon as it fails to prove any theorem. The -a option asks it to keep going and attempt to prove all theorems even if one or more proofs fail.

The -t option specifies a time limit for searching for a proof. For example, -t2 specifies a limit of 2 seconds. The default limit is 5 seconds.

The -x option will cause Natty to export each theorem from the input file (and its dependencies) to a file in the standard THF format. The output files will appear in the thf subdirectory, e.g. in the thf/nat directory for theorems from nat.n. In this mode Natty will not attempt to prove any theorems.

You can also run Natty on a THF file directly:

$ ./natty thf/nat/2_s1.thf

To see a list of other available options, run Natty with no command-line arguments:

$ ./natty

Math library

Natty’s math library is in the math subdirectory, and includes several files:

• nat.n - a definition of the natural numbers plus many theorems about them
• int.n - a definition of the integers based on the natural numbers, plus some theorems about them
• set.n - definitions about sets
• fun.n - definitions about functions
• card.n - cardinality of sets, including a proof of Cantor’s theorem

The theorems and proofs in nat.n and int.n largely follow those in the excellent textbook Number Systems and the Foundations of Analysis (Elliott Mendelson, 1973). However in Mendelson the first natural number is 1 but in Natty’s library it is 0, so I have adapted various proofs accordingly.

There are also files int1.n and num1.n containing more mathematics that Natty can parse and type check but not yet verify, though I am working on that.

Documentation

At this stage there is none, aside from what you see in this README file. I’ll try to improve this over time.

Reading [nat.n]!(nat.n) and other input files may give you an idea of the syntactic constructs that Natty currently understands. You could try running Natty on your own input file with custom axioms and theorems, but be warned that syntax not already present in nat.n or other files is very unlikely to work.

Evaluation

The Python program eval.py evaluates Natty and several other provers (E, Vampire, Zipperposition) on a set of THF files. To use it, first use Natty to export the theorems from nat.n to THF files:

$ natty -x math/nat.n

After that, run

$ python eval.py -pnatty thf/nat

That will run Natty on all the THF files in the nat subdirectory, and generate a results file nat_results.csv that you can open in any spreadsheet program. After ‘-p’ you may alternately specify the name of a different prover to evaluate, one of ‘e’, ‘vampire’ or ‘zipperposition’. Any such prover will need to be in your PATH. To evaluate all of these provers at once, run

$ python eval.py -a thf/nat

References

[^1] !: Bentkamp, Alexander, et al. “Superposition for higher-order logic.” Journal of Automated Reasoning 67.1 (2023): 10.