Help on typing symbols
symboltype
/\
\/
¬!
FFF
TTT
==>
<==
<=>
-->
<->
AA
EE
<=
>=
!=
++
-
xyx y
x+1
y
(x+1)/y

Automated Logic Exercises

Welcome to the seminar!

The goal is to give you an idea of many types of problems that are available. There is much more material than we can cover today, but you can continue at home. Some background topics such as how to use parentheses ( and ) must be introduced, but they are not our focus. They are touched only briefly.

Of course you want to find correct answers, but please also try wrong answers to see what happens! Play with the problems! Type in wrong answers and try to understand why the feedback tool replies as it does!

The feedback tool is a prototype, so please do tolerate minor problems. Suggestions for improvement are welcome! The tool is free for non-commercial use, but if you will use it heavily, please ask first.

And, or, not, and parentheses

We first use the following operators:

symbolreadtype as
and/\
or\/
¬not!

You may also literally write “and”, or even copy and paste the symbol “∧”. Of course, the same applies to the other symbols.

Please notice that “first ∨ second” really means “first or second or both”!

Let B mean that Bern is a nice city, G that Geneva is a nice city, and Z that Zürich is a nice city. Express the following claims.

Zürich is nice.
or

Zürich is bad. (Sorry for this, but also negative examples are needed ☹️)
or

Both Zürich and Bern are nice.
or

How about “Both Bern and Zürich are nice”? Does it mean the same as or different from “Both Zürich and Bern are nice”? Try it on the above and see whether it is correct! helpYou should try “BZ”.

Zürich or Geneva is nice (or both are).
or

All these three cities are nice.
or

At least one of these three cities is nice.
or

Zürich is nice but Bern is not.
or

Parentheses “(” and “)” may be used to express long claims. Here you can try how expressions are structured with and without parentheses. Please experiment with the example written below! Try it, then remove some parentheses, try again, add parentheses somewhere else, and so on. Currently only FF, TT and UU can be used here; sorry for that.
or

A parse tree Now it is your task to get the parentheses to the right place. Please add parentheses so that you get the same picture.

or

We now continue expressing claims.

It is not the case that both Bern and Geneva are nice.
or

Bern or Geneva is bad.
or

Please think about “It is not the case that both Bern and Geneva are nice” and “Bern or Geneva is bad”. Do they mean the same? Try the answer of one in the answer box of the other!

Either Zürich or Geneva is nice, but not both.

or

Often a claim can be expressed in a simpler form. For instance,

this is true if and only ifthis is true
ZZZ
G ∨ (¬GB)GB
B ∧ ¬BF
In mathematics, a claim may be undefined. For instance,
x
0
= 1 is undefined. It is important in programming and computer science to deal appropriately with undefined claims, and the feedback tool can largely do so. Unfortunately, the possibility of undefined claims is usually ignored in logic. Therefore, to keep things simple, today we mostly ignore the possibility of undefined claims.

In the last example, F means that the claim never holds. Indeed, Bern cannot be nice and not nice simultaneously. A claim that always holds can be simplified to T.

symbolreadtype as
FfalseFF
TtrueTT

Be sure not to type F and T as F and T! The latter mean, for instance, that Frankfurt is nice and Torino is nice.

We use “⇔” to denote “simultaneously true”. So the above examples can be re-written as follows:

ZZZ
G ∨ (¬GB)  ⇔  GB
B ∧ ¬BF

Express the following in a simpler form.

¬¬Z  ⇔  or

GBG  ⇔  or

¬GG  ⇔  or

¬F  ⇔  or

¬(GB) ∧ G  ⇔  or

(BZ) ∧ (¬BZ)  ⇔  or

Here you may compare any two propositional formulae, whether they are simultaneously true! You may use any letters, like L for Lausanne.
 ⇔  or

Reasoning operators

A counterexample to a claim on one variable is a value of the variable that makes the claim not hold. For instance, x = −8 is a counterexample to x + 5 ≥ 0.

Please give counterexamples to the following claims. If there are many counterexamples, you may choose yourself which one you give.

Because of a technical limitation of the current version of the tool, here it can only deal reliably with numbers from 0 to 10. (🤓 I will fix it soon, trust me! 🤔) Therefore, these problem types cannot yet be assigned to pupils, but you teachers can live with it. So please only use integers between 0 and 10 (inclusive) as counterexamples.

x + 2 < 9 fails if x =
or

x2 > 0 fails if x =
or

x2 + 10 = 7x fails if x =
or

x2 + 10 ≠ 7x fails if x =
or

A claim is correct if and only if it has no counterexamples.

A reasoning step is of one of the following three forms:

formcounterexample:
a value of the variable that makes
claim1 ⇒ claim2   claim1 hold but claim2 not hold
claim1 ⇐ claim2 claim2 hold but claim1 not hold
claim1 ⇔ claim2 one of claim1 and claim2 hold, and the other not hold

Reasoning steps can be chained, like in claim1 ⇔ claim2 ⇒ claim3. (However, having both ⇒ and ⇐ in the same chain usually does not make sense.)

A reasoning step is correct if and only if it has no counterexamples.

Give counterexamples to the following reasoning steps.

Now you may use also negative numbers and numbers bigger than 10. (On the other hand, now the feedback is less easy to interpret.)

x ≥ 4  ⇒  x ≥ 7
x = or

3 ≥ 2  ⇒  3x ≥ 2x
x = or

x3 = 25x  ⇔  x2 = 25
x = or

x = x − 2  ⇔  x = (x − 2)2.
x = or

Are the following reasoning steps correct?

x < 0  ⇒  x2 > 0
no yes or

x < 0  ⇔  x2 > 0
no yes or

x = x − 2  ⇒  x = −123
no yes or
symbolreadtype as
implies==>
is implied by<==
if and only if<=>

Type the right reasoning operator. If more than one is right, type the most informative one.

x > 4 x ≥ 9
or

x = −3 −2x = 6
or

x = y ax = ay
or

Implication and logical equivalence

Two propositional operators look like reasoning operators.

symbolreadtype as
if then-->
both truth or both false<->

Express the following claims.

If Bern is nice, then also Zürich is nice.
or

Exactly one of Bern and Geneva is nice.
or

Zürich is nice but Bern is not. (This was above, but now you must use → or ↔ or both.)
or

The differences between ⇔ and ↔, or between ⇒ and →, are a long story. Let us just show with an example one difference. (You may modify the example and try again, but please be aware that here the tool computes everything modulo 21. This is yet another imperfection.)

or
or

The issue mentioned in the previous feedback can also be seen from expression trees.

or

Logical Symbols and Equations

We show some examples to illustrate how logical symbols are useful when solving equations.

Logical symbols are nice for expressing more or less than one roots.

Solve the following equations.

x2 − 3x = 0.

or

x − 1 = 1 + x.

or

Reasoning operators are nice for expressing stepwise solutions. A stepwise solution to x2 − 3x = 0 is shown below. Try it first as it is, and then make errors to it, to see what happens.

or

Solve
4x + 7
x2 + 2
= 1. You may write a step, then try it, then add <=> and the next step and so on, until the roots are shown explicitly. If you introduce a fake root, it may be that the tool does not detect it immediately (please remember that the tool is only a prototype!), but it will detect it at the end at the latest.

or

The operator ⇒ is nice for expressing that there may be fake roots that will be eventually filtered out. We use 2x + 3 = x as an example. From now on we show the first ⇔ in the answer box, so that you can change it to ⇒ if wou wish.

or

Please notice how /* and */ were used to add comments to the output, and /**/ to introduce line breaks.

Alternatively, one can add a constrait that rules out the fake roots.

or

Solve
x2x − 20
x − 5
= 11.

or

Logical symbols can also express splitting to cases. To illustrate it, we solve 3|x − 3| = x + 1.

or

Solve 2|x| = x + 2.

or

This kind of splitting to cases is, however, not good for difficult problems, because it forces both cases solved in parallel, or at least one case being carried along while the other is solved. Perhaps sometime in the future the tool makes it possible to solve them separately.

Quantifiers

The most important data structure in programming is an array. It is like a row of boxes numbered consecutively. The numbers of the boxes are indices. Here is an array of characters:

We will, however, work on arrays of numbers. Here is an example:

It is often necessary to express complicated things about arrays. It is possible with quantifiers:

symbolreadtype as
for eachAA
there isEE

Here are some examples on an array A whose indices are 1, …, n:

Every element is 1:
i; 1 ≤ in: A[i] = 1
It is sorted in increasing order:
i; 1 ≤ i < n: A[i] ≤ A[i + 1]
Some element occurs at least twice:
i: ∃ j; 1 ≤ i < jn: A[i] = A[ j]
The smallest element is unique:
i; 1 ≤ in: ∀ j; 1 ≤ jnij: A[i] < A[ j]

Express the following claims on an array A whose indices are 1, …, n.

Every element is less than 2.

or

The array contains at least one zero.

or

The first element is bigger than the others.

or

The array is a palindrome (reads the same forwards and backwards).

or

The array contains at least two distinct elements.

or

Express the following claims as briefly as you can. It may require a lot of thinking! You may proceed in steps.

Try the following filled-in example as such. It first says that some element is bigger than all elements:
i; 1 ≤ in: ∀ j; 1 ≤ jn: A[i] > A[ j]
However, we can reason that if that “some element” is bigger than all elements, then it is bigger than itself, which is impossible. Therefore, this claim is actually logically equivalent to false. The part
F
says that what was claimed before it, is equivalent to false.

or

Now remove <=> FF from the above and try again, to see a message telling that your answer is mathematically correct but not as brief as wanted.

Now you try!

Some element is at least as big as all elements. help 1The biggest element is at least as big as all elements, including itself. help 2You can use the variable n also in other ways than used this far.

or

All elements are equal.

or

Every element is bigger than some other element.

or