oak

Oak is a proof checker focused on simplicity, readability, and ease of use.

For more information, go to oakproof.org.

• Ruby programming language version ≥ 2.0

gem install oakproof

The gem includes E, the external theorem prover used by Oak.

Oak is a command-line application which takes a proof file as input, and tells you whether or not the proof is correct. See oakproof.org for examples and a tutorial.

oak [-v] [-c] [-f] [-m] [-w] <filename>
  -v  print the version number of Oak
  -c  check for unneeded citations
  -f  look for a fix
  -m  assume until marker
  -w  wait for validity (does not change proof outcome)

• The Pulsar text editor (formerly Atom) has a package language-oak which provides syntax highlighting, automatic indentation, and comment toggling for Oak.
• For syntax highlighting on web pages, there is a highlight.js language definition for Oak.
• Similar packages for other editors would be welcome.

• fix issue with gemspec

• converted to a gem, for ease of installation and upgrade

• -m option to assume until marker
• -f option to fix the proof by adding citations
• added ? syntax to find a missing citation
• added proof of number of subsets of a set to set.oak
• new example: descartes.oak

• improved cross-platform portability

• added support for predicates in quantifiers, like for all odd n
• gave iff, if, and implies lower precedence
• new examples: godel_disjunction.oak, product.oak, bernstein.oak, recursion.oak

• new feature: parameterized tie-ins
• new examples: list.oak, graph.oak, konigsberg.oak, leibniz.oak
• moved comprehension axioms into comprehension.oak

• new examples: infinite_primes.oak and set.oak
• merged peano.oak into naturals.oak and expanded
• -w option to wait for validity if unknown
• extra check to ensure A implies A always succeeds
• added not in condition
• added for at most one quantifier
• improved assumption printing
• simplified quantifier variable list syntax
• exit now skips rest of proof, not just current file
• proofs with exit are now marked incomplete

• add "tie-ins" for variables
• -c option to check for unneeded citations
• new examples: kalam.oak and square_root_two.oak
• print notice when exit is called

• performance improvement from internal reworking of scopes/bindings
• variables bound with define can no longer be re-bound in the same scope

• initial release

Many thanks to Stephan Schulz, the author of E, for answering questions and adding options to E to better support Oak.