fmrisc.ProofNavigator.Proving

Class InvalidAnswer

java.lang.Object

fmrisc.ProofNavigator.Proving.AnswerBase

fmrisc.ProofNavigator.Proving.InvalidAnswer

All Implemented Interfaces:

Answer

Direct Known Subclasses:

InvalidAnswerCVCL

public class InvalidAnswer
extends AnswerBase

Answer that formula is invalid.

Constructor Summary

Constructors

Constructor and Description
InvalidAnswer(java.lang.String justification) Create answer that formula is valid with denoted justification.

Method Summary

Modifier and Type	Method and Description
Expression[]	getCounterExample() Interpret justification as a counterexample.

Methods inherited from class fmrisc.ProofNavigator.Proving.AnswerBase

getJustification

Methods inherited from class java.lang.Object

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

Constructor Detail

InvalidAnswer

public InvalidAnswer(java.lang.String justification)

Create answer that formula is valid with denoted justification.

Parameters:

justification - why is formula invalid.

Method Detail

getCounterExample

public Expression[] getCounterExample()

Interpret justification as a counterexample.

Returns:

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