WS18/19 A1 Syntax +

SS18 A1 Syntax +

WS17/18 A1 Syntax +

Takeaways

• You can use a function return value as argument for predicate p(f(x)), but p(p(x)) or f(p(x)) are not valid - p(x) returns nothing in the sense of functions
• You cant use a = operator to compare two isolated sectors with own quantors. You cannot compire two PL statements.

WS20/21 A1 Interpretationen +

SS21 A1 Interpretationen +

WS19/20 A1 Interpretationen +

SS19 A1 Interpretationen +

Falls es leicht war, eine Variabte zu finden, und schwierig, zweite zu finden → Vielleich geht es um eine Tautologie

Es ist fast immer Implikationen. Es wird ausreichen, wenn man so einfach wie moeglich ueberlegt. Fuer F wird man W→F benoetigen, fuer T - alle andere Kombinationen.

WS21/22 A3 Entscheidungsverfahren fuer uninterpretierte Funktionssymbole (Shostak) +

SS21 A3 Entscheidungsverfahren fuer uninterpretierte Funktionssymbole (Shostak) +

WS20/21 A3 Entscheidungsverfahren fuer uninterpretierte Funktionssymbole (Shostak) +

Man darf aus f(g(a)) = f(b) NICHT schliesen, das g(a) = f(b) gilt

Shostak