fmrisc.Proving.CVCL
Class InvalidAnswerCVCL

java.lang.Object
  fmrisc.Proving.AnswerBase
      fmrisc.Proving.InvalidAnswer
          fmrisc.Proving.CVCL.InvalidAnswerCVCL

All Implemented Interfaces:

Answer

public final class InvalidAnswerCVCL
extends InvalidAnswer

Answer that formula is invalid.

Constructor Summary

InvalidAnswerCVCL(CVCL cvcl, java.lang.String justification)
Create answer that formula is valid with denoted justification.

Method Summary

Expression[]

getCounterExample() Interpret justification as a counterexample.

Methods inherited from class fmrisc.Proving.AnswerBase

getJustification

Methods inherited from class java.lang.Object

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

Constructor Detail

InvalidAnswerCVCL

public InvalidAnswerCVCL(CVCL cvcl,
                         java.lang.String justification)

Create answer that formula is valid with denoted justification.

Parameters:

cvcl - CVCL instance that gave the answer

justification - why is formula invalid (may be null)

Method Detail

getCounterExample

public Expression[] getCounterExample()

Interpret justification as a counterexample.

Overrides:

getCounterExample in class InvalidAnswer

Returns:

sequence of formulas whose conjunction represents a refutation (null, if answer cannot be interpreted in this way)