Thanks.
On 21/02/18 11:57, Thomas Tuerk wrote:
> Hi,
>
> the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
> description manual). AC normalisation would sort multiple occurrences of
> the same operant next to each other. Therefore these multiple
> occurrences can then be removed
Hi,
the simplifier supports AC normalisation (see Sec. 7.5.5.2 in the
description manual). AC normalisation would sort multiple occurrences of
the same operant next to each other. Therefore these multiple
occurrences can then be removed by providing 2 idempotency rewrite rules:
f x x = x
f x (f
Hello.
Is there an existing tactic for removing multiple appearances of an
operand under an operator «f» that has the property «f x x = x» and is
associative-commutative? For example, conjunction and disjunction.
If not, I can write one for HOL4, but I do not want to duplicate
existing work.
Second Call for Papers
WiL 2018: Second Women in Logic Workshop
Oxford, UK
8 July 2018
https://sites.google.com/site/womeninlogic2018/welcome/
NEW
* Two invited speakers!
