net.sf.tweety.logics.fol.parser

Class FolParser

java.lang.Object

net.sf.tweety.commons.Parser<FolBeliefSet>

net.sf.tweety.logics.fol.parser.FolParser

public class FolParser
extends Parser<FolBeliefSet>

This class implements a parser for first-order logic. The BNF for a first-order knowledge base is given by (starting symbol is KB)

KB ::== SORTSDEC DECLAR FORMULAS
DECLAR ::== (FUNCTORDEC | PREDDEC)*
SORTSDEC ::== ( SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}" "\n" )*
PREDDEC ::== "type" "(" PREDICATENAME ("(" SORTNAME ("," SORTNAME)* ")")? ")" "\n"
FUNCTORDEC ::== "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" "\n"
FORMULAS ::== ( "\n" FORMULA)*
FORMULA ::== ATOM | "forall" VARIABLENAME ":" "(" FORMULA ")" | "exists" VARIABLENAME ":" "(" FORMULA ")" |
"(" FORMULA ")" | FORMULA "&&" FORMULA | FORMULA "||" FORMULA | "!" FORMULA | "+" | "-"
ATOM ::== PREDICATENAME ("(" TERM ("," TERM)* ")")?
TERM ::== VARIABLENAME | CONSTANTNAME | FUNCTORNAME "(" (TERM ("," TERM)*)? ")"

where SORTNAME, PREDICATENAME, CONSTANTNAME, VARIABLENAME, and FUNCTORNAME are sequences of
symbols from {a,...,z,A,...,Z,0,...,9} with a letter at the beginning.

Author:

Matthias Thimm

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	EXISTS_QUANTIFIER exists-quantifier used in syntax
static java.lang.String	FORALL_QUANTIFIER forall-quantifier used in syntax
private FolSignature	signature Keeps track of the signature.
private java.util.Map<java.lang.String,Variable>	variables Keeps track of variables defined.

Constructor Summary

Constructors

Constructor and Description
FolParser()

Method Summary

Modifier and Type	Method and Description
private void	consumeToken(java.util.Stack<java.lang.Object> stack, int c) This method reads one token from the given reader and appropriately constructs a fol formula from the stream.
FolSignature	getSignature() Returns the signature of this parser.
private FolFormula	parseAtomic(java.util.List<java.lang.Object> l) Parses a simple formula as a list of String tokens or formulas into a fol formula.
FolBeliefSet	parseBeliefBase(java.io.Reader reader) Parses the given reader into a belief base of the given type.
private FolFormula	parseConjunction(java.util.List<java.lang.Object> l) Parses a simple conjunction as a list of String tokens or formulas into a fol formula.
private FolFormula	parseDisjunction(java.util.List<java.lang.Object> l) Parses a disjunction as a list of String tokens or formulas into a fol formula.
Formula	parseFormula(java.io.Reader reader) Parses the given reader into a formula of the given type.
private FolFormula	parseNegation(java.util.List<java.lang.Object> l) Parses a simple formula as a list of String tokens or formulas into a fol formula.
private FolFormula	parseQuantification(java.util.List<java.lang.Object> l) Parses a quantified formula as a list of String tokens or formulas.
void	parseSortDeclaration(java.lang.String s, FolSignature sig) Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.
private java.util.List<Term<?>>	parseTermlist(java.util.List<java.lang.Object> l) Parses a term list as a list of String tokens or terms into a list of terms.
void	parseTypeDeclaration(java.lang.String s, FolSignature sig) Parses a predicate declaration of the form "type" "(" PREDICATENAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" or a functor declaration of the form "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" and modifies the given signature accordingly.
void	setSignature(FolSignature signature) Sets the signature for this parser.

Methods inherited from class net.sf.tweety.commons.Parser

isNumeric, parseBeliefBase, parseBeliefBaseFromFile, parseFormula, parseFormulaFromFile

Methods inherited from class java.lang.Object

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

Field Detail

FORALL_QUANTIFIER

public static final java.lang.String FORALL_QUANTIFIER

forall-quantifier used in syntax

See Also:

Constant Field Values

EXISTS_QUANTIFIER

public static final java.lang.String EXISTS_QUANTIFIER

exists-quantifier used in syntax

See Also:

Constant Field Values

signature

private FolSignature signature

Keeps track of the signature.

variables

private java.util.Map<java.lang.String,Variable> variables

Keeps track of variables defined.

Constructor Detail

FolParser

public FolParser()

Method Detail

parseBeliefBase

public FolBeliefSet parseBeliefBase(java.io.Reader reader)
                             throws java.io.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>

Parameters:

reader - a reader

Returns:

a belief base

Throws:

java.io.IOException

ParserException

parseSortDeclaration

public void parseSortDeclaration(java.lang.String s,
                                 FolSignature sig)
                          throws ParserException

Parses a sort declaration of the form "SORTNAME "=" "{" (CONSTANTNAME ("," CONSTANTNAME)*)? "}"" and modifies the given signature accordingly.

Parameters:

s - a string

sig - a signature

Throws:

ParserException

parseTypeDeclaration

public void parseTypeDeclaration(java.lang.String s,
                                 FolSignature sig)
                          throws ParserException

Parses a predicate declaration of the form "type" "(" PREDICATENAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" or a functor declaration of the form "type" "(" SORTNAME "=" FUNCTORNAME "(" (SORTNAME ("," SORTNAME)*)? ")" ")" and modifies the given signature accordingly.

Parameters:

s - a string

sig - a signature

Throws:

ParserException

parseFormula

public Formula parseFormula(java.io.Reader reader)
                     throws java.io.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>

Parameters:

reader - a reader

Returns:

a formula

Throws:

java.io.IOException

ParserException

consumeToken

private void consumeToken(java.util.Stack<java.lang.Object> stack,
                          int c)
                   throws ParserException

This method reads one token from the given reader and appropriately constructs a fol formula from the stream.

Parameters:

stack - a stack used for monitoring the read items.

c - a token from a stream.

Throws:

ParserException - in case of parser errors.

parseTermlist

private java.util.List<Term<?>> parseTermlist(java.util.List<java.lang.Object> l)
                                       throws ParserException

Parses a term list as a list of String tokens or terms into a list of terms.

Parameters:

l - a list objects, either String tokens or objects of type List.

Returns:

a list of terms.

Throws:

ParserException - if the list could not be parsed.

parseQuantification

private FolFormula parseQuantification(java.util.List<java.lang.Object> l)
                                throws ParserException

Parses a quantified formula as a list of String tokens or formulas.

Parameters:

l - a list objects, either String tokens or objects of type FolFormula.

Returns:

a FolFormula.

Throws:

ParserException - if the list could not be parsed.

parseDisjunction

private FolFormula parseDisjunction(java.util.List<java.lang.Object> l)

Parses a disjunction as a list of String tokens or formulas into a fol formula. This method expects no parentheses in the list and as such treats the formula as a disjunction.

Parameters:

l - a list objects, either String tokens or objects of type FolFormula.

Returns:

a FolFormula.

Throws:

ParserException - if the list could not be parsed.

parseConjunction

private FolFormula parseConjunction(java.util.List<java.lang.Object> l)
                             throws ParserException

Parses a simple conjunction as a list of String tokens or formulas into a fol formula.

Parameters:

l - a list objects, either String tokens or objects of type FolFormula.

Returns:

a FolFormula.

Throws:

ParserException - if the list could not be parsed.

parseNegation

private FolFormula parseNegation(java.util.List<java.lang.Object> l)
                          throws ParserException

Parses a simple formula as a list of String tokens or formulas into a fol formula. This method expects no parentheses, no disjunctions, and no conjunctions in the list and as such treats the formula as a negation.

Parameters:

l - a list objects, either String tokens or objects of type FolFormula.

Returns:

a fol formula.

Throws:

ParserException - if the list could not be parsed.

parseAtomic

private FolFormula parseAtomic(java.util.List<java.lang.Object> l)
                        throws ParserException

Parses a simple formula as a list of String tokens or formulas into a fol formula. This method expects no parentheses, no disjunctions, no conjunctions, and no negation in the list and as such treats the formula as an atomic construct, either a contradiction, a tautology, or an atom (a predicate with a list of terms).

Parameters:

l - a list objects, either String tokens or objects of type folFormula.

Returns:

a fol formula.

Throws:

ParserException

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.