LARA Exercise 04: Predicate Logic and One-Point Rule Forward Symbolic Execution - How to combine program execution and strongest postconditions. First-Order Logic Syntax First-Order Logic Semantics Substitutions for First-Order Logic One-Point Rule (Continued in Lab 04)