## Tutorial 1: Basic Propositional Logic — 20 min

Propositional logic is one of the simplest logical formalisms, which makes a good starting point to get into Redlog.### Domain Selection

```
Reduce (Free CSL version), 19-Aug-15 ...
1: rlset boolean;
*** turned off switch lower
{}{}
2: on rlpcprint;
```

We use rlset to select the relevant
domain, which is called *boolean*. We could also have used its short
name *B*. As a side effect, rlset has
auto-loaded the Redlog package and the relevant domain modules. Functions
with one argument do not require parentheses. On the other hand,
functions with no arguments require an empty pair of parentesis.

The printed message indicates that Reduce has been put into case-sensitive
mode. Note that 3 asterisks "`***`

" indicate an informative
message. In contrast, 5 asterisks "`*****`

" would indicate an
error. The return value of rlset is the
previous domain, which is empty here, because we just started in a fresh
session.

Turning on the switch rlpcprint will allow us to use upper case letters as propositional variables and to ignore the formal construction of propositional logic on the basis of the underlying first-order framework with our first steps here.

### Formula Input

```
3: phi := A or A and B and C;
phi := A or (A and B and C)φ := A ∨ (A ∧ B ∧ C)
4: psi := phi or B and not C and D or false;
psi := (A or (A and B and C)) or (B and not(C) and D) or falseψ := (A ∨ (A ∧ B ∧ C)) ∨ (B ∧ ¬ (C) ∧ D) ∨ false
```

With the definition of `phi`

notice that the operator
and takes precedence over the operator
or. The existing formula `phi`

is reused for defining `psi`

. It is important to understand
that the propositional constants and operators serve as constructors.
There are no implicit logical simplifications. Nevertheless
some *evaluation* takes place here. For instance,
redefining `phi`

would not affect the
existing `psi`

.

### Counting and Analyzing

```
5: length psi;
3
6: part(psi, 1, 2);
A and B and C
7: rlatnum psi;
7
8: rlatl psi;
{A,B,C,D}
9: rlatml psi;
{{A,2},{B,2},{C,2},{D,1}}
```

The length of a formula is the number of arguments of its toplevel operator, which is or here. Since length is a standard Reduce function, it is not prefixed with "rl."

The function part takes an arbitrary number of arguments, which give the path to a subformula. The path can end with \(0\), which denotes the corresponding operator.

rlatnum counts the number of atoms with
multiplicities, which is quite a good measure for the size of a formula.
rlatl gives the list of atoms without
multiplicities, while rlatml returns
a *multiplicity list* associating with each atom the number of its
occurrences.

### Normal Forms and Simplification

```
10: rlsimpl psi;
A or (B and not(C) and D)
11: rlcnf psi;
(A or B) and (A or not(C)) and (A or D)
12: rlnnf not(A and B or not(not C and D));
(not(A) or not(B)) and (not(C) and D)
```

In all domains rlsimpl is the standard simplifier. While for some domains sophisticated simplification techniques might not terminate within reasonable time, rlsimpl generally provides a good tradeoff between efficiency and quality of results. In our example the output happens to be in disjunctive normal form.

rlcnf explicitly computes a conjunctive
normal form. Such normal form computations, like many other Redlog
functions, implicitly apply the standard simplifier in the end. Of course,
there is also rldnf available.
rlnnf computes a *negation normal form*
moving all logical negations towards the atoms.

### Satisfiability and Quantifier Elimination

```
13: rlqe rlex psi;
true
14: rlqe rlall psi;
false
15: rlqe all(a, ex(b, all({c, d}, psi)));
false
16: rlqe all(a, ex(b, psi));
not(C) and D
```

We first solve a classical satisfiability (SAT) problem by using the
existential closure rlex to existentially
quantify all variables occurring in `psi`

and then applying
quantifier elimination to compute a quantifier-free equivalent.
Analogously, universal quantification can be used to decide validity
without explicit reduction to satisfiability via negation.

We can also solve quantified Boolean formula (QBF) problems by making the quantification explicit using the first-order quantifiers ex and rlall. Their first argument is either a variable or a list of variables, which is expanded into several nested quantifiers. The quantifiers require the variables in their first argument to be lower case while the propositional variables establishing atoms must be upper case. Let us not go into detail about this here.

Finally, we can go beyond QBF by even leaving some variables unquantified. The elimination result is then not necessarily true or false but a necessary and sufficient condition in those unquantified variables.

### References

- A. Seidl and T. Sturm. Boolean quantification in a first-order context. Proc. CASC 2003. Technische Universität München, Germany, 2003.
- T. Sturm and C. Zengler. Parametric quantified SAT solving. Proc. ISSAC 2010. ACM Press, 2010.