Package tptp_parser

Interface Summary

Interface	Description
TptpParserOutput	Abstract syntax for TPTP.
TptpParserOutput.Annotations	Must be implemented by a class representing annotations, ie instances of <annotations> in the BNF grammar.
TptpParserOutput.AtomicFormula	Must be implemented by a class representing structures corresponding to instances of <atomic formula> in the BNF grammar.
TptpParserOutput.CnfFormula	Must be implemented by a class representing clause structures corresponding to instances of <cnf formula> in the BNF grammar.
TptpParserOutput.FofFormula	Must be implemented by a class representing formula structures corresponding to instances of <fof formula> in the BNF grammar.
TptpParserOutput.GeneralTerm	Must be implemented by a class representing <general term> in the BNF grammar.
TptpParserOutput.InfoItem	Must be implemented by a class representing instances of <info item> in the BNF grammar.
TptpParserOutput.Literal	Must be implemented by a class representing structures corresponding to instances of <literal> in the BNF grammar.
TptpParserOutput.ParentInfo	Must be implemented by a class representing <parent info> in the BNF grammar.
TptpParserOutput.Source	Must be implemented by a class representing instances of <source> in the BNF grammar.
TptpParserOutput.Term	Must be implemented by a class representing <term> in the BNF grammar.
TptpParserOutput.ThfAtomicFormula	Must be implemented by a class representing structures corresponding to instances of <thf atom> in the BNF grammar.
TptpParserOutput.ThfFormula	Must be implemented by a class representing formula structures corresponding to instances of <thf formula> in the BNF grammar.
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.
TptpTokenTypes

Class Summary

Class	Description
SimpleTptpParserOutput	A simple implementation of the interface TptpParserOutput.
SimpleTptpParserOutput.AnnotatedClause	Represents instances of <cnf annotated> in the BNF grammar.
SimpleTptpParserOutput.AnnotatedFormula	Represents instances of <fof annotated> in the BNF grammar.
SimpleTptpParserOutput.AnnotatedThfFormula	Represents instances of <thf annotated> in the BNF grammar.
SimpleTptpParserOutput.Annotations
SimpleTptpParserOutput.Clause
SimpleTptpParserOutput.Formula
SimpleTptpParserOutput.Formula.Atomic
SimpleTptpParserOutput.Formula.Binary
SimpleTptpParserOutput.Formula.Negation
SimpleTptpParserOutput.Formula.Quantified
SimpleTptpParserOutput.GeneralTerm
SimpleTptpParserOutput.IncludeDirective	Represents instances of <include> in the BNF grammar.
SimpleTptpParserOutput.InfoItem
SimpleTptpParserOutput.InfoItem.AssumptionRecord
SimpleTptpParserOutput.InfoItem.Description
SimpleTptpParserOutput.InfoItem.GeneralFunction
SimpleTptpParserOutput.InfoItem.InferenceRule
SimpleTptpParserOutput.InfoItem.InferenceStatus
SimpleTptpParserOutput.InfoItem.IQuote
SimpleTptpParserOutput.InfoItem.Refutation
SimpleTptpParserOutput.Literal
SimpleTptpParserOutput.ParentInfo
SimpleTptpParserOutput.Source
SimpleTptpParserOutput.Source.Creator
SimpleTptpParserOutput.Source.File
SimpleTptpParserOutput.Source.Inference
SimpleTptpParserOutput.Source.Internal
SimpleTptpParserOutput.Source.ListOfSources
SimpleTptpParserOutput.Source.Name
SimpleTptpParserOutput.Source.Theory
SimpleTptpParserOutput.Symbol
SimpleTptpParserOutput.Term
SimpleTptpParserOutput.ThfFormula
SimpleTptpParserOutput.ThfFormula.ThfAtomic
SimpleTptpParserOutput.ThfFormula.ThfBinary
SimpleTptpParserOutput.ThfFormula.ThfQuantified
SimpleTptpParserOutput.ThfFormula.ThfUnary
SimpleTptpParserOutput.TopLevelItem	A common base for the classes AnnotatedFormula, AnnotatedClause and IncludeDirective.
TptpLexer
TptpParser

Enum Summary

Enum	Description
SimpleTptpParserOutput.Formula.Kind
SimpleTptpParserOutput.InfoItem.Kind
SimpleTptpParserOutput.Source.Kind
SimpleTptpParserOutput.ThfFormula.Kind
TptpParserOutput.BinaryConnective	Reprsents all binary connectives, both associative (&,|) and nonassociative (admissible instances of <binary connective>).
TptpParserOutput.FormulaRole	Reprsents all admissible instances of <formula role> (see the BNF grammar).
TptpParserOutput.IntroType	Reprsents all admissible instances of <intro type> (see the BNF grammar).
TptpParserOutput.Quantifier	Reprsents all quantifiers.
TptpParserOutput.StatusValue	Reprsents all admissible instances of <status value> (see the BNF grammar).
TptpParserOutput.TptpInput.Kind
TptpParserOutput.UnaryConnective	Reprsents all unary connectives, both associative (&,|) and nonassociative (admissible instances of <binary connective>).