Package org.tweetyproject.logics.fol.parser

Class TPTPParser

java.lang.Object

org.tweetyproject.commons.Parser<FolBeliefSet,FolFormula>

org.tweetyproject.logics.fol.parser.TPTPParser

public class TPTPParser
extends Parser<FolBeliefSet,FolFormula>

This class implements a parser for the TPTP syntax that parses single fol formulas and knowledge bases (TPTP problem files or axiom files). TPTP files consist of any of the following in any order and separated by newlines:

• formulas
• comments, i.e. lines starting with "%"
• includes of other TPTP files, i.e. lines like "include('path/to/file',[optional,formula,names])"

The syntax for first-order logic formulas is 'fof(name,role,formula,source,[useful_info]).':

• name is the name of the formula
• role is anything out of {axiom, hypothesis, definition, assumption, lemma, theorem, corollary conjecture, negated_conjecture}
• formula is the actual formula
• The other arguments are optional and ignored by this parser.

Supported operators and pre-defined predicates in formulas:
Negation: ~ formula
Conjunction: formula & formula
Disjunction: formula | formula
Implication: formula => formula
formula <= formula
Equivalence: formula <=> formula
Universal quantifier: ! [Variable1,Variable2,...] : (formula)
Existential quantifier: ? [Variable1,Variable2,...] : (formula)
Tautology: $true
Contradiction: $false
Equality: = (TODO soon to be added)
Inequality: != (TODO soon to be added)

Author:

Anna Gessler

Constructor Summary

Constructors

Constructor	Description
TPTPParser()	Default

Method Summary

Modifier and Type	Method	Description
FolSignature	getSignature()	Returns the signature of this parser.
FolBeliefSet	parseBeliefBase(Reader reader)	Parses the given reader into a belief base of the given type.
FolFormula	parseFormula(Reader reader)	Parses the given reader into a formula of the given type.
void	resetFormulaNames()	Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.
void	resetFormulaRoles()	Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed.
void	setFormulaNames(String formulaNames)	Set the regular expression that restricts which formulas will be parsed.
void	setFormulaRoles(String formulaRoles)	Set the regular expression that restricts which formulas will be parsed.
void	setIncludePath(String includePath)	Set the location of included files.
void	setSignature(FolSignature signature)	Sets the signature for this parser.

Methods inherited from class org.tweetyproject.commons.Parser

isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile, parseListOfBeliefBases, parseListOfBeliefBases, parseListOfBeliefBasesFromFile, parseListOfBeliefBasesFromFile

Methods inherited from class java.lang.Object

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

Constructor Details

TPTPParser

public TPTPParser()

Default

Method Details

parseBeliefBase

public FolBeliefSet parseBeliefBase(Reader reader)
                             throws IOException,
ParserException

Description copied from class: Parser

Parses the given reader into a belief base of the given type.

Specified by:

parseBeliefBase in class Parser<FolBeliefSet,FolFormula>

Parameters:

reader - a reader

Returns:

a belief base

Throws:

IOException - if some IO issue occurred.

ParserException - some parsing exceptions may be added here.

parseFormula

public FolFormula parseFormula(Reader reader)
                        throws IOException,
ParserException

Description copied from class: Parser

Parses the given reader into a formula of the given type.

Specified by:

parseFormula in class Parser<FolBeliefSet,FolFormula>

Parameters:

reader - a reader

Returns:

a formula

Throws:

IOException - if some IO issue occurred.

ParserException - some parsing exceptions may be added here.

setSignature

public void setSignature(FolSignature signature)

Sets the signature for this parser.

Parameters:

signature - a fol signature.

getSignature

public FolSignature getSignature()

Returns the signature of this parser.

Returns:

the signature of this parser.

setFormulaNames

public void setFormulaNames(String formulaNames)

Set the regular expression that restricts which formulas will be parsed. Formulas with names that do not match the expression will not be parsed.

Parameters:

formulaNames - the regex for formula names

setFormulaRoles

public void setFormulaRoles(String formulaRoles)

Set the regular expression that restricts which formulas will be parsed. Formulas with roles that do not match the expression will not be parsed.

Parameters:

formulaRoles - the regex for formula roles

resetFormulaRoles

public void resetFormulaRoles()

Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of any TPTP roles will be parsed. Possible TPTP roles are axiom, hypothesis, definition, assumption, lemma, theorem, corollary, conjecture and negated_conjecture.

resetFormulaNames

public void resetFormulaNames()

Reset the regular expression that restricts which formulas will be parsed to the default value, meaning formulas of all names will be parsed.

setIncludePath

public void setIncludePath(String includePath)

Set the location of included files.

Parameters:

includePath - path that will be prepended to the paths of all included problem files.