added examples; linked to website; fixed bugs

README.md

@@ -1,10 +1,13 @@
 # oak
+
 Oak is a proof checker focused on simplicity, readability, and ease of use.
 
+For downloads and more information, including a tutorial, go to [oakproof.org](http://oakproof.org/).
+
 ## Requirements
 
   * [Ruby programming language](http://ruby-lang.org/)
-  * [E theorem prover](http://eprover.org/) version ≥ 2.0.  Oak expects E's PROVER directory to be in your path.
+  * [E theorem prover](http://eprover.org/) version ≥ 2.0.  E is included in the prepackaged Oak downloads available at [oakproof.org](http://oakproof.org/).  If you prefer to install E yourself, be sure to add E's PROVER directory to your system's PATH variable so that Oak will detect it.
 
 ## Usage
 
@@ -13,6 +16,6 @@ oak [-v] [filename]
     -v  print the version number of Oak
 ```
 
-## Tutorial
+## Acknowledgements
 
-Coming soon...
+Many thanks to Stephan Schulz, the author of E, for answering questions and adding options to E to better support Oak.

examples/naturals.oak

@@ -0,0 +1,30 @@
+/#
+	Results about natural numbers.  Needs expansion!
+#/
+
+include "peano.oak"
+
+# natural numbers are closed under addition
+nat_closed_addition: for all a,b in N, a+b is in N
+proof
+  # define a property to be used for induction
+  P_def: for some P, for all a in N,
+    P(a) iff for all b in N, a+b is in N
+      by comprehension
+
+  P(0) by P_def, peano  # base case
+
+  1: take any a in N
+    2: suppose P(a)  # induction hypothesis
+      3: take any b in N
+        a+b is in N by P_def, 1, 2, 3
+        so (a+b)+1 is in N by peano
+        so (a+1)+b is in N by peano, 1, 3
+      end
+      so P(a+1) by P_def, peano, 1
+    end
+  end
+
+  so for all a in N, P(a) by induction
+  so thesis by P_def
+end

examples/peano.oak

@@ -0,0 +1,32 @@
+/#
+	"Enhanced" Peano axioms adapted from:
+
+		Kaye, Richard (1991).  Models of Peano Arithmetic.  Pages 16-18.
+
+	We include a comprehension schema for definitions.  This also allows
+	induction to be a statement rather than a schema.
+#/
+
+peano: axiom
+
+	0 is in N 																and (
+	1 is in N																) and (
+	for all x in N, x+1 is in N 						) and (
+
+	for all x,y,z in N, (x+y)+z = x+(y+z)		) and (  #  + is associative
+	for all x,y in N, x+y = y+x							) and (  #  + is commutative
+	for all x,y,z in N, (x*y)*z = x*(y*z)		) and (  #  * is associative
+	for all x,y in N, x*y = y*x							) and (  #  * is commutative
+	for all x,y,z in N, x*(y+z) = x*y + x*z	) and (  #  * distributes over +
+	for all x in N, x+0 = x and x*0 = 0			) and (	 #  identity of 0
+	for all x in N, x*1 = x									)				 #  identity of 1
+
+induction: axiom for all P,
+	if 	P[0] and
+			for all n in N, P[n] implies P[n+1]
+	then
+			for all n in N, P[n]
+
+comprehension: axiom schema
+	for all meta P,n,φ such that not free[P,φ],
+		`for some P, for all n in N, P[n] iff φ`

lib/external prover.rb

@@ -172,7 +172,7 @@ def valid_e? tree
 		settings << '--detsort-rw --detsort-new' # make it deterministic
 
 		# use local copy if there is one, otherwise call it without a path
-		local = File.expand_path '../eprover/eprover', File.dirname(__FILE__)
+		local = File.expand_path '../eprover/PROVER/eprover', File.dirname(__FILE__)
 		location = File.exist?(local) ? local : 'eprover'
 
 		output = `"#{location}" #{settings.join ' '} --auto --tptp3-format -s #{file_path} 2>&1`

lib/oak.rb

@@ -101,7 +101,6 @@ def initialize
 		@active_reason_sets = [[]]
 		@scopes = []
 		@theses = []
-		@parser = Parser.new
 		@label_stack = [[]]
     @line_numbers_by_label = {}
 		@inactive_labels = Set[]
@@ -245,13 +244,14 @@ def end_block
 		end
 	end
 
-	def include input, is_filename = false
-		if is_filename
-			filename = input
+	def include input, is_path = false
+		if is_path
+			dirname = File.dirname input
+			filename = File.basename input
 			begin
-				input = File.read filename
+				input = File.read input
 			rescue
-				puts "error: could not open file \"#{filename}\""
+				puts "error: could not open file \"#{input}\""
 				raise ProofException
 			end
 		else
@@ -262,7 +262,7 @@ def include input, is_filename = false
 			line_number = nil # external scope, for error reporting
 			from_include = false
 			wrapper.print "#{filename}: processing line "
-			@parser.parse_each(input) {|sentence, action, content, reasons, label, fileline|
+			Parser.new.parse_each(input) {|sentence, action, content, reasons, label, fileline|
 				next if action == :empty
 				break if action == :exit
 				line_number = fileline
@@ -271,6 +271,8 @@ def include input, is_filename = false
 				id = {:label => label, :filename => filename, :fileline => fileline}
 				case action
 					when :include then
+						# include relative to path of current proof file
+						content = File.expand_path content, dirname if is_path
 						wrapper.puts
 						from_include = true
 						include content, :is_filename

oak

@@ -1,10 +1,8 @@
-DIR="$(dirname "$0")"
+DIR=$(dirname "$0")
 
-# use local ruby if available
-if [ -d "$DIR/ruby" ]; then
-	RUBY=$DIR/ruby/bin/ruby
+if hash ruby 2>/dev/null; then
+  ruby "$DIR/lib/oak.rb" "$@"  
 else
-	RUBY=ruby
+  echo "error: could not find \"ruby\""
+	echo "Oak requires the Ruby programming language to be installed."
 fi
-
-$RUBY $DIR/lib/oak.rb "$@"