fmrisc.ProgramExplorer.Proving

Class ClassicalProblem

java.lang.Object

fmrisc.ProgramExplorer.Proving.ClassicalProblem

public class ClassicalProblem
extends java.lang.Object

A proving problem in classical logic.

Constructor Summary

Constructors

Constructor and Description
ClassicalProblem(Declaration[] decls, Formula goal, ErrorStream out) Construct a proving problem.

Method Summary

Modifier and Type	Method and Description
Declaration[]	getDeclarations() Get the declarations.
Formula	getGoal() Get the goal.
void	print(java.io.PrintWriter out) Print task to output stream.
ProofNavigatorProblem	proofNavigatorProblem(java.io.File dir) Translate classical problem to RISC ProofNavigator Problem

Methods inherited from class java.lang.Object

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

Constructor Detail

ClassicalProblem

public ClassicalProblem(Declaration[] decls,
                        Formula goal,
                        ErrorStream out)

Construct a proving problem.

Parameters:

decls - the declarations of entities refered in the goal.

goal - the goal to be proved.

out - a stream for printing messages.

Method Detail

print

public void print(java.io.PrintWriter out)

Print task to output stream.

Parameters:

out - the stream to print to

getDeclarations

public Declaration[] getDeclarations()

Get the declarations.

Returns:

the declarations.

getGoal

public Formula getGoal()

Get the goal.

Returns:

the goal.

proofNavigatorProblem

public ProofNavigatorProblem proofNavigatorProblem(java.io.File dir)

Translate classical problem to RISC ProofNavigator Problem

Parameters:

dir - the directory to which information may be written

Returns:

the translation.