(Dis)Equality Constraints (Bsp, Def)

∧ (a_n = b_n∧b_n = a_n+1∨a_n = c_n∧c_n = a_n+1)

∧ a_n+1≠a₀

(Quelle: Strichman, Rozanov, SMT Workshop 2007, http://www.lsi.upc.edu/~oliveras/espai/smtSlides/ofer.ppt, http://smtexec.org/exec/smtlib-portal-benchmarks.php?download&inline&b=QF_UF/eq_diamond/Feq_diamond10.smt2

Formel ∃x₁,…, x_n : M mathend000# mit M mathend000# in negationstechnischer Normalform über Signatur:

• Prädikatsymbole = mathend000# und ≠ mathend000#, keine Funktionssymbole