Package org.svvrl.goal.core.logic.propositional

Class PLImplication

java.lang.Object

org.svvrl.goal.core.logic.Logic

org.svvrl.goal.core.logic.propositional.PL

org.svvrl.goal.core.logic.propositional.PLBinary

org.svvrl.goal.core.logic.propositional.PLImplication

All Implemented Interfaces:

java.io.Serializable, java.lang.Cloneable

public class PLImplication
extends PLBinary

This class defines an implication formula l → r where l and r are propositional formulae.

Author:

Ming-Hsien Tsai

See Also:

Serialized Form

Field Summary

Fields inherited from class org.svvrl.goal.core.logic.propositional.PLBinary

left, op_string, right

Fields inherited from class org.svvrl.goal.core.logic.propositional.PL

FALSE, TRUE

Constructor Summary

Constructors

Constructor	Description
PLImplication(PL l, PL r)	Constructs an implication formula l → r where l and r are two specified propositional formulae.

Method Summary

Modifier and Type	Method	Description
PLImplication	clone()
PL	evaluate(java.util.Map<Proposition,java.lang.Boolean> m)	Evaluates this formula.
PL	getNegationNormalForm()	Returns the negation normal form of this formula.
int	getPrecedence()	Returns the precedence of the operator of this formula.
PLBinary	newInstance(PL l, PL r)	Returns a binary formula l º r where º is the same as the binary operator of this formula, and l and r are two specified propositional formulae.
PL	pushNegation()	Pushes a negation into this formula as deep as possible.

Methods inherited from class org.svvrl.goal.core.logic.propositional.PLBinary

equals, getFreeVariables, getLeftSubFormula, getRightSubFormula, toString

Methods inherited from class org.svvrl.goal.core.logic.propositional.PL

evaluate, fromCNF, fromConjunction, fromDisjunction, fromDNF, fromLiteral, hashCode

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Details

PLImplication

public PLImplication(PL l, PL r)

Constructs an implication formula l → r where l and r are two specified propositional formulae.

Parameters:

l - a propositional formula

r - a propositional formula

Method Details

getPrecedence

public int getPrecedence()

Description copied from class: PL

Returns the precedence of the operator of this formula.

Specified by:

getPrecedence in class PL

Returns:

the precedence of the operator of this formula

pushNegation

public PL pushNegation()

Description copied from class: PL

Pushes a negation into this formula as deep as possible. This method should be used for classical propositional logic.

Specified by:

pushNegation in class PL

Returns:

a formula obtained by pushing a negation into this formula as deep as possible

getNegationNormalForm

public PL getNegationNormalForm()

Description copied from class: PL

Returns the negation normal form of this formula. This method should be used for classical propositional logic.

Overrides:

getNegationNormalForm in class PLBinary

Returns:

the negation normal form of this formula

evaluate

public PL evaluate(java.util.Map<Proposition,java.lang.Boolean> m)

Description copied from class: PL

Evaluates this formula.

Specified by:

evaluate in class PL

Parameters:

m - an (partial) interpretation of propositions

Returns:

a formula obtained by changing every proposition p to m(p)

newInstance

public PLBinary newInstance(PL l, PL r)

Description copied from class: PLBinary

Returns a binary formula l º r where º is the same as the binary operator of this formula, and l and r are two specified propositional formulae.

Specified by:

newInstance in class PLBinary

Parameters:

l - a propositional formula

r - a propositional formula

Returns:

a binary formula l º r where º is the same as the binary operator of this formula

clone

public PLImplication clone()

Overrides:

clone in class java.lang.Object