java.lang.Object
- net.sf.tweety.arg.adf.transform.DefinitionalCNFTransform

All Implemented Interfaces:

Transform<Disjunction,Proposition>
```
public class DefinitionalCNFTransform
extends java.lang.Object
implements Transform<Disjunction,Proposition>
```
An implementation of a definitional (resp. Tseitin) CNF transformation algorithm. It avoids potential exponential blowup by the idea of naming subformulas. This works via the introduction of fresh propositional variables which are then defined s.t. their truth values match their corresponding subformulas.
Example:
Formula: a v b
Fresh variable: n
Define n: n <-> a v b
Clauses: (-n v a v b), (-a v n), (-b v n)
Now n is defined and can be used at occurences of (a v b). For instance, instead of generating clauses for (a v b) -> c, we can continue generating clauses for n -> c.
Note that this implementation also provides an optimized version which is disabled by default but can be enabled with a constructor parameter. This optimization does not always generate full definitions, i.e. n <-> (a v b), but based on the polarity either n -> (a v b) resp. (a v b) -> n. This generates less clauses but does not guarantee satisfiability-equivalence if it is used in the context of other formulas. It should therefore only be used if the transformed formula does not appear in the context of other formulas or if it appears only at positions with positive polarity.
Example: Let f be an arbitrary formula which we translate using this implementation. We then get a name to f, say fn, and a set of clauses which represents f, say Cf. If we plan to use fn in some context like (fn -> a) v (-fn -> b) together with Cf, we are fine if we use the non-optimized version. However, the optimized version makes assumptions on the positions of the subformulas, if we thus change the context, these assumptions may no longer be true. In this example fn is used at a positive and at a negative position, which is not permitted.

Author:

Mathias Hofer

Field Summary

Fields
Modifier and Type Field Description

private java.util.function.Function<Argument,Proposition> argumentToProposition

private boolean optimize

Constructor Summary

Constructors
Constructor	Description
`DefinitionalCNFTransform(java.util.function.Function<Argument,Proposition> argumentToProposition)`	Constructs a non-optimized version of the definitional (resp.
`DefinitionalCNFTransform(java.util.function.Function<Argument,Proposition> argumentToProposition, boolean optimize)`	Constructs a possibly optimized version of the definitional (resp.

Method Summary

Modifier and Type	Method	Description
`Proposition`	`transformArgument(java.util.function.Consumer<Disjunction> consumer, Argument argument, int polarity)`	This method is visited by the `Arguments` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformConjunction(java.util.function.Consumer<Disjunction> consumer, java.util.Collection<Proposition> subconditions, int polarity)`	This method is visited by the `ConjunctionAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformContradiction(java.util.function.Consumer<Disjunction> consumer, int polarity)`	This method is visited by the `ContradictionAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformDisjunction(java.util.function.Consumer<Disjunction> consumer, java.util.Collection<Proposition> subconditions, int polarity)`	This method is visited by the `DisjunctionAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformEquivalence(java.util.function.Consumer<Disjunction> consumer, Proposition left, Proposition right, int polarity)`	This method is visited by the `EquivalenceAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformExclusiveDisjunction(java.util.function.Consumer<Disjunction> consumer, Proposition left, Proposition right, int polarity)`	This method is visited by the `ExclusiveDisjunctionAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformImplication(java.util.function.Consumer<Disjunction> consumer, Proposition left, Proposition right, int polarity)`	This method is visited by the `ImplicationAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformNegation(java.util.function.Consumer<Disjunction> consumer, Proposition sub, int polarity)`	This method is visited by the `NegationAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.
`Proposition`	`transformTautology(java.util.function.Consumer<Disjunction> consumer, int polarity)`	This method is visited by the `TautologyAcceptanceConditions` of the acceptance condition on which we apply this `Transform`.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - argumentToProposition
```
private java.util.function.Function<Argument,Proposition> argumentToProposition
```
  - optimize
```
private boolean optimize
```
- Constructor Detail
  - DefinitionalCNFTransform
```
public DefinitionalCNFTransform(java.util.function.Function<Argument,Proposition> argumentToProposition)
```
    Constructs a non-optimized version of the definitional (resp. Tseitin) CNF transformation algorithm.
    
    Parameters:
    
    argumentToProposition - mapping used to transform the arguments to propositions.
  - DefinitionalCNFTransform
```
public DefinitionalCNFTransform(java.util.function.Function<Argument,Proposition> argumentToProposition,
                                boolean optimize)
```
    Constructs a possibly optimized version of the definitional (resp. Tseitin) CNF transformation algorithm.
    The optimization generates only the necessary parts of the definitions based on the polarity of the subformulas, i.e. <- or -> (or both for polarity = 0) instead of always <->.
    
    Parameters:
    
    argumentToProposition - mapping used to transform the arguments to propositions.
    
    optimize - true enables the optimized definition
- Method Detail
  - transformDisjunction
```
public Proposition transformDisjunction(java.util.function.Consumer<Disjunction> consumer,
                                        java.util.Collection<Proposition> subconditions,
                                        int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the DisjunctionAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformDisjunction in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    subconditions - the subconditions of this disjunction, e.g. {a, b} if this = or(a,b)
    
    polarity - polarity < 0: negative global position of this disjunction, e.g. this -> a
    polarity = 0: neutral global position of this disjunction, e.g. this <-> a
    polarity > 0: positive global position of this disjunction, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this disjunction
  - transformConjunction
```
public Proposition transformConjunction(java.util.function.Consumer<Disjunction> consumer,
                                        java.util.Collection<Proposition> subconditions,
                                        int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the ConjunctionAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformConjunction in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    subconditions - the subconditions of this conjunction, e.g. {a, b} if this = and(a,b)
    
    polarity - polarity < 0: negative global position of this conjunction, e.g. this -> a
    polarity = 0: neutral global position of this conjunction, e.g. this <-> a
    polarity > 0: positive global position of this conjunction, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this conjunction
  - transformImplication
```
public Proposition transformImplication(java.util.function.Consumer<Disjunction> consumer,
                                        Proposition left,
                                        Proposition right,
                                        int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the ImplicationAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformImplication in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    left - the left part of the implication
    
    right - the right part of the implication
    
    polarity - polarity < 0: negative global position of this implication, e.g. this -> a
    polarity = 0: neutral global position of this implication, e.g. this <-> a
    polarity > 0: positive global position of this implication, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this implication
  - transformEquivalence
```
public Proposition transformEquivalence(java.util.function.Consumer<Disjunction> consumer,
                                        Proposition left,
                                        Proposition right,
                                        int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the EquivalenceAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformEquivalence in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    left - the left part of the equivalence
    
    right - the right part of the equivalence
    
    polarity - polarity < 0: negative global position of this equivalence, e.g. this -> a
    polarity = 0: neutral global position of this equivalence, e.g. this <-> a
    polarity > 0: positive global position of this equivalence, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this equivalence
  - transformExclusiveDisjunction
```
public Proposition transformExclusiveDisjunction(java.util.function.Consumer<Disjunction> consumer,
                                                 Proposition left,
                                                 Proposition right,
                                                 int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the ExclusiveDisjunctionAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformExclusiveDisjunction in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    left - the left part of the xor
    
    right - the right part of the xor
    
    polarity - polarity < 0: negative global position of this xor, e.g. this -> a
    polarity = 0: neutral global position of this xor, e.g. this <-> a
    polarity > 0: positive global position of this xor, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this xor
  - transformNegation
```
public Proposition transformNegation(java.util.function.Consumer<Disjunction> consumer,
                                     Proposition sub,
                                     int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the NegationAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformNegation in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    sub - the subformula of this negation, i.e. this = neg(sub)
    
    polarity - polarity < 0: negative global position of this negation, e.g. this -> a
    polarity = 0: neutral global position of this negation, e.g. this <-> a
    polarity > 0: positive global position of this negation, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this negation
  - transformArgument
```
public Proposition transformArgument(java.util.function.Consumer<Disjunction> consumer,
                                     Argument argument,
                                     int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the Arguments of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformArgument in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    argument - the argument which calls this method
    
    polarity - polarity < 0: negative global position of this argument, e.g. this -> a
    polarity = 0: neutral global position of this argument, e.g. this <-> a
    polarity > 0: positive global position of this argument, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this argument
  - transformContradiction
```
public Proposition transformContradiction(java.util.function.Consumer<Disjunction> consumer,
                                          int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the ContradictionAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformContradiction in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    polarity - polarity < 0: negative global position of this contradiction, e.g. this -> a
    polarity = 0: neutral global position of this contradiction, e.g. this <-> a
    polarity > 0: positive global position of this contradiction, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this contradiction
  - transformTautology
```
public Proposition transformTautology(java.util.function.Consumer<Disjunction> consumer,
                                      int polarity)
```
    Description copied from interface: Transform
    
    This method is visited by the TautologyAcceptanceConditions of the acceptance condition on which we apply this Transform.
    
    Specified by:
    
    transformTautology in interface Transform<Disjunction,Proposition>
    
    Parameters:
    
    consumer - the consumer of the computed return values
    
    polarity - polarity < 0: negative global position of this tautology, e.g. this -> a
    polarity = 0: neutral global position of this tautology, e.g. this <-> a
    polarity > 0: positive global position of this tautology, e.g. a -> this
    
    Returns:
    
    the result which we want to return to the parent-formula of this tautology

Modifier and Type	Field	Description
`private java.util.function.Function<Argument,Proposition>`	`argumentToProposition`
`private boolean`	`optimize`

Class DefinitionalCNFTransform

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

argumentToProposition

optimize

Constructor Detail

DefinitionalCNFTransform

DefinitionalCNFTransform

Method Detail

transformDisjunction

transformConjunction

transformImplication

transformEquivalence

transformExclusiveDisjunction

transformNegation

transformArgument

transformContradiction

transformTautology