# Question:Two questions about Logic package and a strange result

## Question:Two questions about Logic package and a strange result

Maple 2015

Hi,

First question
Let P1 the logical proposition

```restart
with(Logic):
local O
P1 := (&not O) &and (&not C) &implies (&not Q);
```

Is it possible to obtain its contraposition P2  in a form that contains &implies?

```# P2 := (Q) &implies &not ((&not O) &and (&not C));
```

Second question
Why does the modulo 2 canonical form of proposition P5 above contains "1" "plus" other terms:
(if 1 is present this means 1 + something = 1 and then that P5 is a tautology, which is obviously wrong as Tautology(P5) shows)

```restart
with(Logic):
local O
P1 := (&not O) &and (&not C) &implies (&not Q);-
P2 := (Q) &implies &not ((&not O) &and (&not C));
P3 := op(1, P2) &and (&not C);
P4 := op(2, P2) &and (&not C);
P5 := P3 &implies P4:

Canonicalize(P5, {O, C, Q}, form=MOD2)

C O Q + C Q + O Q + Q + 1

```

Verificaion of what the modulo 2 canonical form of a proposition including an "addititive" tautology is

```T := O &or (&not O):
Canonicalize(T, {O}, form=MOD2);
Canonicalize(T &or S, {O, S}, form=MOD2);
1
1
```

Is it that I missed something or is iot a bug?

Watchout: this result has been obtained with Maple 2015.2

TIA

﻿