(Dis)Equality Constraints (Bsp, Def)

		(a₀ = b₀ $\displaystyle \wedge$ b₀ = a₁ $\displaystyle \vee$ a₀ = c₀ $\displaystyle \wedge$ c₀ = a₁) $\displaystyle \wedge$ ...
	$\displaystyle \wedge$	(a_n = b_n $\displaystyle \wedge$ b_n = a_n+1 $\displaystyle \vee$ a_n = c_n $\displaystyle \wedge$ c_n = a_n+1)
	$\displaystyle \wedge$	a_n+1 $\displaystyle \neq$ a₀

(Quelle: Strichman, Rozanov, SMT Workshop 2007, http://www.lsi.upc.edu/~oliveras/espai/smtSlides/ofer.ppt, http://www.smtexec.org/exec/benchmarkDetail.php?benchmark=661781)

Formel $\exists$ x₁,..., x_n : M mit M in negationstechnischer Normalform über Signatur:

Prädikatsymbole = und $\neq$ , keine Funktionssymbole

2009-06-22