EC/UF

EC: Equality-Constraints

• Definieren Sie die Syntax von EC (durch Angabe einer Signatur)
• Geben Sie je ein Beispiel für ein erfüllbares und ein nicht erfüllbares EC mit zwei Variablen an.
• Beweisen Sie: (*) für alle C∈EC mathend000# mit n mathend000# Variablen gilt:

  C mathend000# besitzt Modell $\iff$ mathend000# C mathend000# besitzt Modell mit Universum der Größe ≤n mathend000#.

UF: EC mit uninterpretierten Funktionen

• Geben Sie ein UF-Constraint an, für das (*) nicht gilt.
• (Zusatz): gilt UF(*) mit einer anderen Schranke (als ≤n mathend000#)?