public class FormulaTask extends ClassicalTaskBase
Task.Observer, Task.Status
Constructor and Description |
---|
FormulaTask(FormulaDefinition formula,
TheorySymbol theory,
java.io.File parent,
ErrorStream out)
Construct a task.
|
Modifier and Type | Method and Description |
---|---|
ClassicalProblem |
classicalProblem()
Translate task into a classical proving problem
|
proofNavigatorProblem, reset
setParent
getDirectory, getEvidence, getInfo, getName, getParent, getParentDirectory, getPosition, getStatus, isFinal, isOptional, print, resume, resumeOnNew, setDirectory, setObserver, setStatus
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, print, resume, resumeOnNew, setObserver, setParent, setStatus
public FormulaTask(FormulaDefinition formula, TheorySymbol theory, java.io.File parent, ErrorStream out)
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 errorspublic ClassicalProblem classicalProblem()