SAV07 Homework 1
Here is the Homework 1 PDF (with some corrected typos).
Here are some example ocaml programs that may help you get started with using ocaml (but see also http://caml.inria.fr/ ). Please remove the .txt extension when saving the file.
Note that you will need to use a slightly different syntax tree compared to one in formulas.ml, because the quantifiers in your homework are bounded.
See also Notes on Context-Free Grammars.
Here is SAV07 Homework 1 Solution for the theoretical part.
NOTE: A formula of the form
forall x < 0. F
should always evaluate to true when x ranges over non-negative integers, regardless of F. Namely, there are no such non-negative x, so this is the case of a bounded quantifier over an empty set. This formula is trivially true because it is equivalent to
forall x. false -> F