Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav07_homework_1 [2007/03/23 06:10]
vkuncak
sav07_homework_1 [2007/04/12 21:34] (current)
vkuncak
Line 12: Line 12:
  
 Here is [[SAV07 Homework 1 Solution]] for the theoretical part. 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
 
© EPFL 2018 - Legal notice