Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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