Lab for Automated Reasoning and Analysis LARA

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 ). 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, 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
sav07_homework_1.txt · Last modified: 2007/04/12 21:34 by vkuncak