/oak

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

Primary LanguageRubyGNU Affero General Public License v3.0AGPL-3.0

oak

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

For more information, go to oakproof.org.

Requirements

Installation

gem install oakproof

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

Usage

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)

Editor support

  • 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.

Version history

v0.7.2 - 2024-06-22

  • fix issue with gemspec

v0.7.1 - 2024-06-21

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

v0.7 - 2024-05-16

  • -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

v0.6.1 - 2023-08-10

  • improved cross-platform portability

v0.6 - 2023-07-09

  • 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

v0.5 - 2022-04-19

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

v0.4 - 2021-04-17

  • 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

v0.3 - 2020-12-22

  • 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

v0.2 - 2019-08-08

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

v0.1 - 2017-08-31

  • initial release

Acknowledgements

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