fmrisc.ProgramExplorer.Tasks

Class FormulaTask

java.lang.Object

fmrisc.ProgramExplorer.Tasks.TaskBase

fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

fmrisc.ProgramExplorer.Tasks.FormulaTask

All Implemented Interfaces:

ClassicalTask, ProofNavigatorTask, Task

public class FormulaTask
extends ClassicalTaskBase

The task of proving a user-defined formula.

Nested Class Summary

Nested classes/interfaces inherited from interface fmrisc.ProgramExplorer.Tasks.Task

Task.Observer, Task.Status

Constructor Summary

Constructors

Constructor and Description
FormulaTask(FormulaDefinition formula, TheorySymbol theory, java.io.File parent, ErrorStream out) Construct a task.

Method Summary

Methods

Modifier and Type	Method and Description
ClassicalProblem	classicalProblem() Translate task into a classical proving problem

Methods inherited from class fmrisc.ProgramExplorer.Tasks.ClassicalTaskBase

proofNavigatorProblem, reset

Methods inherited from class fmrisc.ProgramExplorer.Tasks.ProofNavigatorTaskBase

setParent

Methods inherited from class fmrisc.ProgramExplorer.Tasks.TaskBase

getDirectory, getEvidence, getInfo, getName, getParent, getParentDirectory, getPosition, getStatus, isFinal, isOptional, print, resume, resumeOnNew, setDirectory, setObserver, setStatus

Methods inherited from class java.lang.Object

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

Methods inherited from interface fmrisc.ProgramExplorer.Tasks.Task

getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, print, resume, resumeOnNew, setObserver, setParent, setStatus

Constructor Detail

FormulaTask

public FormulaTask(FormulaDefinition formula,
           TheorySymbol theory,
           java.io.File parent,
           ErrorStream out)

Construct a task.

Parameters:

formula - the definition of the formula to be proved.

theory - the theory in which the definition occurs.

parent - the parent directory.

out - stream for printing errors

Method Detail

classicalProblem

public ClassicalProblem classicalProblem()

Translate task into a classical proving problem

Returns:

the translation.