- English only

# Lab for Automated Reasoning and Analysis LARA

# Homework 03: Solutions

## Problem 1

Let be the set of all first-order formulas (viewed as syntax trees, so e.g. is a different formula from and let be the implication relation on formulas:

Check whether is reflexive, antisymmetric, and transitive relation.

### Solution

The relation is both reflexive and transitive.

It is not antisymmetric. As a counterexample consider the example that is given in the problem statement: and

## Problem 2

Let be a partial order such that every set has the greatest lower bound. Prove that then every set has the least upper bound.

## Problem 3

Galois connection is defined by two monotonic functions and between partial orders on and on , such that

for all and (intuitively, the condition means that is approximated by ).

**Part a)** Show that the condition is equivalent to the conjunction of these two conditions:

hold for all and .

**Part b)** Let and satisfy the condition of Galois connection. Show that the following three conditions are equivalent:

- for all
- is a surjective function
- is an injective function

## Problem 4

Consider Problem 3 on the Space of Invariants in the **previous homework, Homework 02**.

**a):** Is the set a lattice? If it is a lattice, is it complete? If it is not a lattice, can it be modified to become a lattice?

**b):** From now on, fix the relation . Define and define . Are functions and monotonic? Do they form a Galois connection? Prove or give a counterexample.

**c):** For each of the functions , , describe the space of prefix points, postfix points, as well as the least and the greatest fixpoints. You may find Fixed Point Theorems useful.