TptpParserOutput (sigma-component 2.10 API)

All Known Implementing Classes:

SimpleTptpParserOutput
```
public interface TptpParserOutput
```
Abstract syntax for TPTP. Most of the features declared here are used by the TPTP parser to communicate the results of parsing. The user of the parser is supposed to provide implementations of the interfaces declared here (for many users the default implementation in SimpleTptpParserOutput.java may be good enough). Such approach is taken to nicely isolate the grammar sources from the environment. It makes the parser highly alienable. A new user only has to provide an implementation of these interfaces in order to link the parser to his/her code. No matter how the data returned from the parser is processed, no modification of the parser code is required. The requirements imposed by the interface are quite liberal, so that writing modules glueing the parser with practically any application is easy.

Since:

Feb 02, 2006, Nov 13, 2007 ("package tptp_parser;" added by AR)

Author:

Alexandre Riazanov

Nested Class Summary

Nested Classes
Modifier and Type	Interface and Description
`static interface`	`TptpParserOutput.Annotations` Must be implemented by a class representing annotations, ie instances of <annotations> in the BNF grammar.
`static interface`	`TptpParserOutput.AtomicFormula` Must be implemented by a class representing structures corresponding to instances of <atomic formula> in the BNF grammar.
`static class`	`TptpParserOutput.BinaryConnective` Reprsents all binary connectives, both associative (&,\|) and nonassociative (admissible instances of <binary connective>).
`static interface`	`TptpParserOutput.CnfFormula` Must be implemented by a class representing clause structures corresponding to instances of <cnf formula> in the BNF grammar.
`static interface`	`TptpParserOutput.FofFormula` Must be implemented by a class representing formula structures corresponding to instances of <fof formula> in the BNF grammar.
`static class`	`TptpParserOutput.FormulaRole` Reprsents all admissible instances of <formula role> (see the BNF grammar).
`static interface`	`TptpParserOutput.GeneralTerm` Must be implemented by a class representing <general term> in the BNF grammar.
`static interface`	`TptpParserOutput.InfoItem` Must be implemented by a class representing instances of <info item> in the BNF grammar.
`static class`	`TptpParserOutput.IntroType` Reprsents all admissible instances of <intro type> (see the BNF grammar).
`static interface`	`TptpParserOutput.Literal` Must be implemented by a class representing structures corresponding to instances of <literal> in the BNF grammar.
`static interface`	`TptpParserOutput.ParentInfo` Must be implemented by a class representing <parent info> in the BNF grammar.
`static class`	`TptpParserOutput.Quantifier` Reprsents all quantifiers.
`static interface`	`TptpParserOutput.Source` Must be implemented by a class representing instances of <source> in the BNF grammar.
`static class`	`TptpParserOutput.StatusValue` Reprsents all admissible instances of <status value> (see the BNF grammar).
`static interface`	`TptpParserOutput.Term` Must be implemented by a class representing <term> in the BNF grammar.
`static interface`	`TptpParserOutput.ThfAtomicFormula` Must be implemented by a class representing structures corresponding to instances of <thf atom> in the BNF grammar.
`static interface`	`TptpParserOutput.ThfFormula` Must be implemented by a class representing formula structures corresponding to instances of <thf formula> in the BNF grammar.
`static interface`	`TptpParserOutput.TptpInput` Must be implemented by a class representing instances of <TPTP input> in the BNF grammar (except comments), ie top level input items, such as annotated formulas and include directives.
`static class`	`TptpParserOutput.UnaryConnective` Reprsents all unary connectives, both associative (&,\|) and nonassociative (admissible instances of <binary connective>).

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method and Description
`TptpParserOutput.FofFormula`	`atomAsFormula(TptpParserOutput.AtomicFormula atom)` A correct implementation must return an object of the class implementing FofFormula, representing the atomic formula represented by the object atom .
`TptpParserOutput.ThfFormula`	`atomAsThfFormula(TptpParserOutput.ThfAtomicFormula atom)` A correct implementation must return an object of the class implementing ThfFormula, representing the atomic formula represented by the object atom .
`TptpParserOutput.AtomicFormula`	`builtInFalse()` A correct implementation must return a representation for $false.
`TptpParserOutput.ThfFormula`	`builtInThfFalse()`
`TptpParserOutput.ThfFormula`	`builtInThfTrue()`
`TptpParserOutput.AtomicFormula`	`builtInTrue()` A correct implementation must return a representation for $true.
`TptpParserOutput.Annotations`	`createAnnotations(TptpParserOutput.Source source, Iterable<TptpParserOutput.InfoItem> usefulInfo)` A correct implementation must return an object representing an instance of <annotations> composed of source and usefulInfo .
`TptpParserOutput.InfoItem`	`createAssumptionRecordInfoItem(Iterable<String> nameList)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <assumption record> with a list <name list> as the parameter.
`TptpParserOutput.FofFormula`	`createBinaryFormula(TptpParserOutput.FofFormula lhs, TptpParserOutput.BinaryConnective connective, TptpParserOutput.FofFormula rhs)` A correct implementation must return an object representing the binary formula obtained by applying connective to lhs and rhs .
`TptpParserOutput.CnfFormula`	`createClause(Iterable<TptpParserOutput.Literal> literals)` A correct implementation must return an object representing the clause made of literals .
`TptpParserOutput.TptpInput`	`createCnfAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.CnfFormula clause, TptpParserOutput.Annotations annotations, int lineNumber)` A correct implementation must return a TptpInput object representing clause wrapped in the corresponding annotation.
`TptpParserOutput.InfoItem`	`createDescriptionInfoItem(String singleQuoted)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <description item> with the specified parameter.
`TptpParserOutput.AtomicFormula`	`createEqualityAtom(TptpParserOutput.Term lhs, TptpParserOutput.Term rhs)` A correct implementation must return an object representing the atomic formula obtained by applying the equality predicate to the terms.
`TptpParserOutput.TptpInput`	`createFofAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.FofFormula formula, TptpParserOutput.Annotations annotations, int lineNumber)` A correct implementation must return a TptpInput object representing formula wrapped in the corresponding annotation.
`TptpParserOutput.GeneralTerm`	`createGeneralCnfFormula(TptpParserOutput.CnfFormula formula)` A correct implementation must return an object representing a formula
`TptpParserOutput.GeneralTerm`	`createGeneralColon(TptpParserOutput.GeneralTerm left, TptpParserOutput.GeneralTerm right)` A correct implementation must return an object representing a general term obtained by applying ':' (colon) binary operator to two general terms.
`TptpParserOutput.GeneralTerm`	`createGeneralDistinctObject(String str)` A correct implementation must return an object representing a general term constructed as a number or a double-quoted string (both represented as a string)
`TptpParserOutput.GeneralTerm`	`createGeneralFofFormula(TptpParserOutput.FofFormula formula)` A correct implementation must return an object representing a formula
`TptpParserOutput.GeneralTerm`	`createGeneralFunction(String function, Iterable<TptpParserOutput.GeneralTerm> arguments)` A correct implementation must return an object representing the non-list term obtained by applying function to arguments .
`TptpParserOutput.InfoItem`	`createGeneralFunctionInfoItem(TptpParserOutput.GeneralTerm generalFunction)` A correct implementation must return an object representing an instance of <info item> corresponding to the specified instance of <general function>.
`TptpParserOutput.GeneralTerm`	`createGeneralList(Iterable<TptpParserOutput.GeneralTerm> list)` A correct implementation must return an object representing the general term constructed as a list.
`TptpParserOutput.GeneralTerm`	`createGeneralTerm(TptpParserOutput.Term term)` A correct implementation must return an object representing a formula
`TptpParserOutput.GeneralTerm`	`createGeneralThfFormula(TptpParserOutput.ThfFormula formula)` A correct implementation must return an object representing a formula
`TptpParserOutput.GeneralTerm`	`createGeneralVariable(String var)` A correct implementation must return an object representing a general term constructed as a variable (represented as a string)
`TptpParserOutput.TptpInput`	`createIncludeDirective(String fileName, Iterable<String> formulaSelection, int lineNumber)` A correct implementation must return a TptpInput object representing the instance of <include> with the specified parameters.
`TptpParserOutput.InfoItem`	`createInferenceRuleInfoItem(String inferenceRule, String inferenceId, Iterable<TptpParserOutput.GeneralTerm> attributes)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <inference info> with the specified constituents.
`TptpParserOutput.InfoItem`	`createInferenceStatusInfoItem(TptpParserOutput.StatusValue statusValue)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of status(<status value>) with the specified parameter.
`TptpParserOutput.Source`	`createInternalSource(String introType, Iterable<TptpParserOutput.InfoItem> introInfo)` A correct implementation must return an object representing an instance of <source> corresponding to an instance of <internal source> with the specified constituents.
`TptpParserOutput.InfoItem`	`createIQuoteInfoItem(String singleQuoted)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <iquote item> with the specified parameter.
`TptpParserOutput.Literal`	`createLiteral(boolean positive, TptpParserOutput.AtomicFormula atom)` A correct implementation must return an object representing the literal with atom and the polarity determined by positive .
`TptpParserOutput.FofFormula`	`createNegationOf(TptpParserOutput.FofFormula formula)` A correct implementation must return an object representing the formula obtained by applying the negation connective to formula .
`TptpParserOutput.ParentInfo`	`createParentInfo(TptpParserOutput.Source source, TptpParserOutput.GeneralTerm parentDetails)` A correct implementation must return an object representing the parent info item with the specified parameters.
`TptpParserOutput.AtomicFormula`	`createPlainAtom(String predicate, Iterable<TptpParserOutput.Term> arguments)` A correct implementation must return an object representing the atomic formula obtained by applying predicate to arguments .
`TptpParserOutput.Term`	`createPlainTerm(String function, Iterable<TptpParserOutput.Term> arguments)` A correct implementation must return an object representing the non-variable term obtained by applying function to arguments .
`TptpParserOutput.FofFormula`	`createQuantifiedFormula(TptpParserOutput.Quantifier quantifier, Iterable<String> variableList, TptpParserOutput.FofFormula formula)` A correct implementation must return an object representing the formula obtained by applying the quantifier quantifier to formula .
`TptpParserOutput.InfoItem`	`createRefutationInfoItem(TptpParserOutput.Source fileSource)` A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <refutation> with the specified parameter.
`TptpParserOutput.Source`	`createSourceFromCreator(String creatorName, Iterable<TptpParserOutput.InfoItem> usefulInfo)` A correct implementation must return an object representing an instance of <source> corresponding to the specified creator.
`TptpParserOutput.Source`	`createSourceFromFile(String fileName, String fileInfo)` A correct implementation must return an object representing an instance of <source> corresponding to the specified location in a file.
`TptpParserOutput.Source`	`createSourceFromInferenceRecord(String inferenceRule, Iterable<TptpParserOutput.InfoItem> usefulInfo, Iterable<TptpParserOutput.ParentInfo> parentInfoList)` A correct implementation must return an object representing an instance of <source> corresponding to an instance of <inference record> with the specified constituents.
`TptpParserOutput.Source`	`createSourceFromListOfSources(Iterable<TptpParserOutput.Source> listOfSources)` A correct implementation must return an object representing an instance of <source> corresponding to a list of <sources> with the specified constituents.
`TptpParserOutput.Source`	`createSourceFromName(String name)` A correct implementation must return an object representing an instance of <source> corresponding to name .
`TptpParserOutput.Source`	`createSourceFromTheory(String theoryName, Iterable<TptpParserOutput.InfoItem> usefulInfo)` A correct implementation must return an object representing an instance of <source> corresponding to the specified theory.
`TptpParserOutput.AtomicFormula`	`createSystemAtom(String predicate, Iterable<TptpParserOutput.Term> arguments)` A correct implementation must return an object representing the atomic formula obtained by applying predicate to arguments .
`TptpParserOutput.Term`	`createSystemTerm(String function, Iterable<TptpParserOutput.Term> arguments)` A correct implementation must return an object representing the atomic formula obtained by applying function to arguments .
`TptpParserOutput.TptpInput`	`createThfAnnotated(String name, TptpParserOutput.FormulaRole role, TptpParserOutput.ThfFormula formula, TptpParserOutput.Annotations annotations, int lineNumber)` A correct implementation must return a TptpInput object representing formula wrapped in the corresponding annotation.
`TptpParserOutput.ThfFormula`	`createThfBinaryFormula(TptpParserOutput.ThfFormula lhs, TptpParserOutput.BinaryConnective connective, TptpParserOutput.ThfFormula rhs)` A correct implementation must return an object representing the binary formula obtained by applying connective to lhs and rhs .
`TptpParserOutput.ThfFormula`	`createThfPlainAtom(String predicate, Iterable<TptpParserOutput.Term> arguments)`
`TptpParserOutput.ThfFormula`	`createThfQuantifiedFormula(TptpParserOutput.Quantifier quantifier, Iterable<TptpParserOutput.ThfFormula> variableList, TptpParserOutput.ThfFormula formula)` A correct implementation must return an object representing the formula obtained by applying the quantifier quantifier to formula .
`TptpParserOutput.ThfFormula`	`createThfSystemAtom(String predicate, Iterable<TptpParserOutput.Term> arguments)`
`TptpParserOutput.ThfFormula`	`createThfUnaryOf(TptpParserOutput.UnaryConnective unary, TptpParserOutput.ThfFormula formula)` A correct implementation must return an object representing the formula obtained by applying the negation connective to formula .
`TptpParserOutput.ThfFormula`	`createThfVariableAtom(String variable)`
`TptpParserOutput.Term`	`createVariableTerm(String variable)` A correct implementation must return an object representing variable as a term.

- Method Detail
  - createThfAnnotated
```
TptpParserOutput.TptpInput createThfAnnotated(String name,
                                              TptpParserOutput.FormulaRole role,
                                              TptpParserOutput.ThfFormula formula,
                                              TptpParserOutput.Annotations annotations,
                                              int lineNumber)
```
    A correct implementation must return a TptpInput object representing formula wrapped in the corresponding annotation.
    
    Parameters:
    
    name - != null
    
    role - != null
    
    formula - != null
    
    annotations - can be null
    
    lineNumber - location in the input
  - createFofAnnotated
```
TptpParserOutput.TptpInput createFofAnnotated(String name,
                                              TptpParserOutput.FormulaRole role,
                                              TptpParserOutput.FofFormula formula,
                                              TptpParserOutput.Annotations annotations,
                                              int lineNumber)
```
    A correct implementation must return a TptpInput object representing formula wrapped in the corresponding annotation.
    
    Parameters:
    
    name - != null
    
    role - != null
    
    formula - != null
    
    annotations - can be null
    
    lineNumber - location in the input
  - createCnfAnnotated
```
TptpParserOutput.TptpInput createCnfAnnotated(String name,
                                              TptpParserOutput.FormulaRole role,
                                              TptpParserOutput.CnfFormula clause,
                                              TptpParserOutput.Annotations annotations,
                                              int lineNumber)
```
    A correct implementation must return a TptpInput object representing clause wrapped in the corresponding annotation.
    
    Parameters:
    
    name - != null
    
    role - != null
    
    clause - != null
    
    annotations - can be null
    
    lineNumber - location in the input
  - createIncludeDirective
```
TptpParserOutput.TptpInput createIncludeDirective(String fileName,
                                                  Iterable<String> formulaSelection,
                                                  int lineNumber)
```
    A correct implementation must return a TptpInput object representing the instance of <include> with the specified parameters.
    
    Parameters:
    
    fileName - != null
    
    formulaSelection - satisfies (formulaSelection == null || formulaSelection.iterator().hasNext())
    
    lineNumber - location in the input
  - createThfBinaryFormula
```
TptpParserOutput.ThfFormula createThfBinaryFormula(TptpParserOutput.ThfFormula lhs,
                                                   TptpParserOutput.BinaryConnective connective,
                                                   TptpParserOutput.ThfFormula rhs)
```
    A correct implementation must return an object representing the binary formula obtained by applying connective to lhs and rhs . Note that the method must work with conjunction and disjunction, as well as with nonassociative connectives.
    
    Parameters:
    
    lhs - != null
    
    connective - != null
    
    rhs - != null
  - createThfUnaryOf
```
TptpParserOutput.ThfFormula createThfUnaryOf(TptpParserOutput.UnaryConnective unary,
                                             TptpParserOutput.ThfFormula formula)
```
    A correct implementation must return an object representing the formula obtained by applying the negation connective to formula .
    
    Parameters:
    
    formula - != null
  - createThfQuantifiedFormula
```
TptpParserOutput.ThfFormula createThfQuantifiedFormula(TptpParserOutput.Quantifier quantifier,
                                                       Iterable<TptpParserOutput.ThfFormula> variableList,
                                                       TptpParserOutput.ThfFormula formula)
```
    A correct implementation must return an object representing the formula obtained by applying the quantifier quantifier to formula .
    
    Parameters:
    
    quantifier - != null
    
    variableList - != null && variableList.iterator().hasNext()
    
    formula - != null
  - atomAsThfFormula
```
TptpParserOutput.ThfFormula atomAsThfFormula(TptpParserOutput.ThfAtomicFormula atom)
```
    A correct implementation must return an object of the class implementing ThfFormula, representing the atomic formula represented by the object atom .
    
    Parameters:
    
    atom - != null
  - createThfPlainAtom
```
TptpParserOutput.ThfFormula createThfPlainAtom(String predicate,
                                               Iterable<TptpParserOutput.Term> arguments)
```
  - createThfSystemAtom
```
TptpParserOutput.ThfFormula createThfSystemAtom(String predicate,
                                                Iterable<TptpParserOutput.Term> arguments)
```
  - builtInThfTrue
```
TptpParserOutput.ThfFormula builtInThfTrue()
```
  - builtInThfFalse
```
TptpParserOutput.ThfFormula builtInThfFalse()
```
  - createThfVariableAtom
```
TptpParserOutput.ThfFormula createThfVariableAtom(String variable)
```
  - createBinaryFormula
```
TptpParserOutput.FofFormula createBinaryFormula(TptpParserOutput.FofFormula lhs,
                                                TptpParserOutput.BinaryConnective connective,
                                                TptpParserOutput.FofFormula rhs)
```
    A correct implementation must return an object representing the binary formula obtained by applying connective to lhs and rhs . Note that the method must work with conjunction and disjunction, as well as with nonassociative connectives.
    
    Parameters:
    
    lhs - != null
    
    connective - != null
    
    rhs - != null
  - createNegationOf
```
TptpParserOutput.FofFormula createNegationOf(TptpParserOutput.FofFormula formula)
```
    A correct implementation must return an object representing the formula obtained by applying the negation connective to formula .
    
    Parameters:
    
    formula - != null
  - createQuantifiedFormula
```
TptpParserOutput.FofFormula createQuantifiedFormula(TptpParserOutput.Quantifier quantifier,
                                                    Iterable<String> variableList,
                                                    TptpParserOutput.FofFormula formula)
```
    A correct implementation must return an object representing the formula obtained by applying the quantifier quantifier to formula .
    
    Parameters:
    
    quantifier - != null
    
    variableList - != null && variableList.iterator().hasNext()
    
    formula - != null
  - createClause
```
TptpParserOutput.CnfFormula createClause(Iterable<TptpParserOutput.Literal> literals)
```
    A correct implementation must return an object representing the clause made of literals . literals will always be null if an empty clause has to be created.
    
    Parameters:
    
    literals - satisfies (literals == null || literals.iterator().hasNext())
  - atomAsFormula
```
TptpParserOutput.FofFormula atomAsFormula(TptpParserOutput.AtomicFormula atom)
```
    A correct implementation must return an object of the class implementing FofFormula, representing the atomic formula represented by the object atom .
    
    Parameters:
    
    atom - != null
  - createLiteral
```
TptpParserOutput.Literal createLiteral(boolean positive,
                                       TptpParserOutput.AtomicFormula atom)
```
    A correct implementation must return an object representing the literal with atom and the polarity determined by positive .
    
    Parameters:
    
    positive - == true iff the literal has to be positive
    
    atom - != null
  - createPlainAtom
```
TptpParserOutput.AtomicFormula createPlainAtom(String predicate,
                                               Iterable<TptpParserOutput.Term> arguments)
```
    A correct implementation must return an object representing the atomic formula obtained by applying predicate to arguments . arguments will always be null if there are no arguments.
    
    Parameters:
    
    predicate - != null
    
    arguments - satisfies (arguments == null || arguments.iterator().hasNext())
  - createSystemAtom
```
TptpParserOutput.AtomicFormula createSystemAtom(String predicate,
                                                Iterable<TptpParserOutput.Term> arguments)
```
    A correct implementation must return an object representing the atomic formula obtained by applying predicate to arguments . arguments will always be null if there are no arguments.
    
    Parameters:
    
    predicate - != null
    
    arguments - satisfies (arguments == null || arguments.iterator().hasNext())
  - createEqualityAtom
```
TptpParserOutput.AtomicFormula createEqualityAtom(TptpParserOutput.Term lhs,
                                                  TptpParserOutput.Term rhs)
```
    A correct implementation must return an object representing the atomic formula obtained by applying the equality predicate to the terms.
  - builtInTrue
```
TptpParserOutput.AtomicFormula builtInTrue()
```
    A correct implementation must return a representation for $true.
  - builtInFalse
```
TptpParserOutput.AtomicFormula builtInFalse()
```
    A correct implementation must return a representation for $false.
  - createVariableTerm
```
TptpParserOutput.Term createVariableTerm(String variable)
```
    A correct implementation must return an object representing variable as a term.
    
    Parameters:
    
    variable - != null
  - createPlainTerm
```
TptpParserOutput.Term createPlainTerm(String function,
                                      Iterable<TptpParserOutput.Term> arguments)
```
    A correct implementation must return an object representing the non-variable term obtained by applying function to arguments . arguments will always be null if there are no arguments, ie when the term is an individual constant.
    
    Parameters:
    
    function - != null
    
    arguments - satisfies (arguments == null || arguments.iterator().hasNext())
  - createSystemTerm
```
TptpParserOutput.Term createSystemTerm(String function,
                                       Iterable<TptpParserOutput.Term> arguments)
```
    A correct implementation must return an object representing the atomic formula obtained by applying function to arguments . arguments will always be null if there are no arguments, ie when the term is an individual constant.
    
    Parameters:
    
    function - != null
    
    arguments - satisfies (arguments == null || arguments.iterator().hasNext())
  - createAnnotations
```
TptpParserOutput.Annotations createAnnotations(TptpParserOutput.Source source,
                                               Iterable<TptpParserOutput.InfoItem> usefulInfo)
```
    A correct implementation must return an object representing an instance of <annotations> composed of source and usefulInfo .
    
    Parameters:
    
    source - != null
    
    usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())
  - createSourceFromName
```
TptpParserOutput.Source createSourceFromName(String name)
```
    A correct implementation must return an object representing an instance of <source> corresponding to name .
    
    Parameters:
    
    name - != null
  - createSourceFromListOfSources
```
TptpParserOutput.Source createSourceFromListOfSources(Iterable<TptpParserOutput.Source> listOfSources)
```
    A correct implementation must return an object representing an instance of <source> corresponding to a list of <sources> with the specified constituents.
    
    Parameters:
    
    listOfSources - nonempty
  - createSourceFromInferenceRecord
```
TptpParserOutput.Source createSourceFromInferenceRecord(String inferenceRule,
                                                        Iterable<TptpParserOutput.InfoItem> usefulInfo,
                                                        Iterable<TptpParserOutput.ParentInfo> parentInfoList)
```
    A correct implementation must return an object representing an instance of <source> corresponding to an instance of <inference record> with the specified constituents.
    
    Parameters:
    
    inferenceRule - != null
    
    usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())
    
    parentInfoList - nonempty
  - createInternalSource
```
TptpParserOutput.Source createInternalSource(String introType,
                                             Iterable<TptpParserOutput.InfoItem> introInfo)
```
    A correct implementation must return an object representing an instance of <source> corresponding to an instance of <internal source> with the specified constituents.
    
    Parameters:
    
    introType - != null
    
    introInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())
  - createSourceFromFile
```
TptpParserOutput.Source createSourceFromFile(String fileName,
                                             String fileInfo)
```
    A correct implementation must return an object representing an instance of <source> corresponding to the specified location in a file.
    
    Parameters:
    
    fileName - != null
    
    fileInfo - (may be null)
  - createSourceFromCreator
```
TptpParserOutput.Source createSourceFromCreator(String creatorName,
                                                Iterable<TptpParserOutput.InfoItem> usefulInfo)
```
    A correct implementation must return an object representing an instance of <source> corresponding to the specified creator.
    
    Parameters:
    
    creatorName - != null
    
    usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())
  - createSourceFromTheory
```
TptpParserOutput.Source createSourceFromTheory(String theoryName,
                                               Iterable<TptpParserOutput.InfoItem> usefulInfo)
```
    A correct implementation must return an object representing an instance of <source> corresponding to the specified theory.
    
    Parameters:
    
    theoryName - != null
    
    usefulInfo - satisfies (usefulInfo == null || usefulInfo.iterator().hasNext())
  - createDescriptionInfoItem
```
TptpParserOutput.InfoItem createDescriptionInfoItem(String singleQuoted)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <description item> with the specified parameter.
    
    Parameters:
    
    singleQuoted - != null
  - createIQuoteInfoItem
```
TptpParserOutput.InfoItem createIQuoteInfoItem(String singleQuoted)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <iquote item> with the specified parameter.
    
    Parameters:
    
    singleQuoted - != null
  - createInferenceStatusInfoItem
```
TptpParserOutput.InfoItem createInferenceStatusInfoItem(TptpParserOutput.StatusValue statusValue)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of status(<status value>) with the specified parameter.
    
    Parameters:
    
    statusValue - != null
  - createAssumptionRecordInfoItem
```
TptpParserOutput.InfoItem createAssumptionRecordInfoItem(Iterable<String> nameList)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <assumption record> with a list <name list> as the parameter.
    
    Parameters:
    
    nameList - != null
  - createInferenceRuleInfoItem
```
TptpParserOutput.InfoItem createInferenceRuleInfoItem(String inferenceRule,
                                                      String inferenceId,
                                                      Iterable<TptpParserOutput.GeneralTerm> attributes)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <inference info> with the specified constituents.
    
    Parameters:
    
    inferenceRule - != null
    
    inferenceId - != null
    
    attributes - satisfies (attributes == null || attributes.iterator().hasNext())
  - createRefutationInfoItem
```
TptpParserOutput.InfoItem createRefutationInfoItem(TptpParserOutput.Source fileSource)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to an instance of <refutation> with the specified parameter.
    
    Parameters:
    
    fileSource - returned by a call to createSourceFromFile(..)
  - createGeneralFunctionInfoItem
```
TptpParserOutput.InfoItem createGeneralFunctionInfoItem(TptpParserOutput.GeneralTerm generalFunction)
```
    A correct implementation must return an object representing an instance of <info item> corresponding to the specified instance of <general function>.
    
    Parameters:
    
    generalFunction - returned by a call to createGeneralFunction(..)
  - createGeneralFunction
```
TptpParserOutput.GeneralTerm createGeneralFunction(String function,
                                                   Iterable<TptpParserOutput.GeneralTerm> arguments)
```
    A correct implementation must return an object representing the non-list term obtained by applying function to arguments . arguments will always be null if there are no arguments, ie when the term is an individual constant.
    
    Parameters:
    
    function - != null
    
    arguments - satisfies (arguments == null || arguments.iterator().hasNext())
  - createGeneralList
```
TptpParserOutput.GeneralTerm createGeneralList(Iterable<TptpParserOutput.GeneralTerm> list)
```
    A correct implementation must return an object representing the general term constructed as a list.
    
    Parameters:
    
    list - satisfies (list == null || list.iterator().hasNext())
  - createGeneralColon
```
TptpParserOutput.GeneralTerm createGeneralColon(TptpParserOutput.GeneralTerm left,
                                                TptpParserOutput.GeneralTerm right)
```
    A correct implementation must return an object representing a general term obtained by applying ':' (colon) binary operator to two general terms. Left operand should be not a list.
    
    Parameters:
    
    left - should not be a general term presenting a list
    
    righ -
  - createGeneralDistinctObject
```
TptpParserOutput.GeneralTerm createGeneralDistinctObject(String str)
```
    A correct implementation must return an object representing a general term constructed as a number or a double-quoted string (both represented as a string)
    
    Parameters:
    
    str -
  - createGeneralVariable
```
TptpParserOutput.GeneralTerm createGeneralVariable(String var)
```
    A correct implementation must return an object representing a general term constructed as a variable (represented as a string)
    
    Parameters:
    
    str -
  - createGeneralThfFormula
```
TptpParserOutput.GeneralTerm createGeneralThfFormula(TptpParserOutput.ThfFormula formula)
```
    A correct implementation must return an object representing a formula
    
    Parameters:
    
    formula -
  - createGeneralFofFormula
```
TptpParserOutput.GeneralTerm createGeneralFofFormula(TptpParserOutput.FofFormula formula)
```
    A correct implementation must return an object representing a formula
    
    Parameters:
    
    formula -
  - createGeneralCnfFormula
```
TptpParserOutput.GeneralTerm createGeneralCnfFormula(TptpParserOutput.CnfFormula formula)
```
    A correct implementation must return an object representing a formula
    
    Parameters:
    
    formula -
  - createGeneralTerm
```
TptpParserOutput.GeneralTerm createGeneralTerm(TptpParserOutput.Term term)
```
    A correct implementation must return an object representing a formula
    
    Parameters:
    
    formula -
  - createParentInfo
```
TptpParserOutput.ParentInfo createParentInfo(TptpParserOutput.Source source,
                                             TptpParserOutput.GeneralTerm parentDetails)
```
    A correct implementation must return an object representing the parent info item with the specified parameters.
    
    Parameters:
    
    source - != null
    
    parentDetails - if nonnull, corresponds to <single quoted> in the -<single quoted> option in the BNF rule for <parent details> when parentDetails = null, it corresponds to the <null> option in that rule

Interface TptpParserOutput

Nested Class Summary

Method Summary

Method Detail

createThfAnnotated

createFofAnnotated

createCnfAnnotated

createIncludeDirective

createThfBinaryFormula

createThfUnaryOf

createThfQuantifiedFormula

atomAsThfFormula

createThfPlainAtom

createThfSystemAtom

builtInThfTrue

builtInThfFalse

createThfVariableAtom

createBinaryFormula

createNegationOf

createQuantifiedFormula

createClause

atomAsFormula

createLiteral

createPlainAtom

createSystemAtom

createEqualityAtom

builtInTrue

builtInFalse

createVariableTerm

createPlainTerm

createSystemTerm

createAnnotations

createSourceFromName

createSourceFromListOfSources

createSourceFromInferenceRecord

createInternalSource

createSourceFromFile

createSourceFromCreator

createSourceFromTheory

createDescriptionInfoItem

createIQuoteInfoItem

createInferenceStatusInfoItem

createAssumptionRecordInfoItem

createInferenceRuleInfoItem

createRefutationInfoItem

createGeneralFunctionInfoItem

createGeneralFunction

createGeneralList

createGeneralColon

createGeneralDistinctObject

createGeneralVariable

createGeneralThfFormula

createGeneralFofFormula

createGeneralCnfFormula

createGeneralTerm

createParentInfo