Package owl.translations.mastertheorem

Class Normalisation

java.lang.Object

owl.translations.mastertheorem.Normalisation

All Implemented Interfaces:

Function<LabelledFormula,LabelledFormula>, UnaryOperator<LabelledFormula>

public final class Normalisation
extends Object
implements UnaryOperator<LabelledFormula>

Δ₂-Normalisation according to Bibliography.LICS_20 with minor tweaks skipping unnecessary rewrite steps.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	Normalisation.NormalisationMethod

Method Summary

Modifier and Type	Method	Description
Formula	apply(Formula formula)
LabelledFormula	apply(LabelledFormula labelledFormula)
static boolean	isPi2OrFgPi1(Formula.TemporalOperator temporalOperator)
static boolean	isSigma2OrGfSigma1(Formula.TemporalOperator temporalOperator)
static Normalisation	of(Normalisation.NormalisationMethod method, boolean strict)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface java.util.function.Function

andThen, compose

Method Detail

of

public static Normalisation of(Normalisation.NormalisationMethod method,
                               boolean strict)

isSigma2OrGfSigma1

public static boolean isSigma2OrGfSigma1(Formula.TemporalOperator temporalOperator)

isPi2OrFgPi1

public static boolean isPi2OrFgPi1(Formula.TemporalOperator temporalOperator)

apply

public LabelledFormula apply(LabelledFormula labelledFormula)

Specified by:

apply in interface Function<LabelledFormula,LabelledFormula>

apply

public Formula apply(Formula formula)