Package net.sf.tweety.logics.ml.parser

Class MlParser

  • public class MlParser
extends Parser<MlBeliefSet,​RelationalFormula>
    This class implements a parser for modal logic. The BNF for a modal 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 | "+" | "-" |
    FORMULA "=>" FORMULA | FORMULA "<=>" FORMULA | FORMULA "==" FORMULA | FORMULA "/==" FORMULA |
    "[]" "(" FORMULA ")" | "<>" "(" FORMULA ")"
    ATOM ::== PREDICATENAME ("(" TERM ("," TERM)* ")")?
    TERM ::== VARIABLENAME | CONSTANTNAME | FUNCTORNAME "(" (TERM ("," TERM)*)? ")"

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

    Note: Equality/Inequality predicates ("==" and "/==") can only be parsed if the parser is given a FolSignature
    with equality (which is not the case by default).
    Author:
    Matthias Thimm, Anna Gessler

    • Field Summary

      Fields 
      Modifier and Type Field Description
      (package private) FolParser folparser
      First-order logic parser used for parsing sorts and type declaration.

    • Constructor Summary

      Constructors 
      Constructor Description
      MlParser()  

    • Method Summary

      Modifier and Type Method 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 modal formula from the stream.
      FolSignature getSignature()
      Returns the signature of this parser.
      private RelationalFormula parseAtomic​(java.util.List<java.lang.Object> l)
      Parses a simple formula as a list of String tokens or formulas into a fol formula.
      MlBeliefSet parseBeliefBase​(java.io.Reader reader)
      Parses the given reader into a belief base of the given type.
      private RelationalFormula 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 RelationalFormula parseDisjunction​(java.util.List<java.lang.Object> l)
      Parses a disjunction as a list of String tokens or formulas into a fol formula.
      private RelationalFormula parseEquivalence​(java.util.List<java.lang.Object> l)
      Parses an equivalence as a list of String tokens or formulas into a fol formula.
      RelationalFormula parseFormula​(java.io.Reader reader)
      Parses the given reader into a formula of the given type.
      private RelationalFormula parseImplication​(java.util.List<java.lang.Object> l)
      Parses an implication as a list of String tokens or formulas into a fol formula.
      private RelationalFormula parseModalization​(java.util.List<java.lang.Object> l)
      Parses a formula containing at least one modal operator as a list of String tokens or formulas.
      private RelationalFormula 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 RelationalFormula parseQuantification​(java.util.List<java.lang.Object> l)
      Parses a quantified formula as a list of String tokens or formulas.
      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 setSignature​(FolSignature signature)
      Sets the signature for this parser.

      • Methods inherited from class java.lang.Object

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

    • Field Detail

      • folparser

        FolParser folparser
        First-order logic parser used for parsing sorts and type declaration.

    • Constructor Detail

      • MlParser

        public MlParser()

    • Method Detail

      • 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 modal 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)
        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 RelationalFormula 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.

      • parseModalization

        private RelationalFormula parseModalization​(java.util.List<java.lang.Object> l)
                                     throws ParserException
        Parses a formula containing at least one modal operator 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.

      • parseEquivalence

        private RelationalFormula parseEquivalence​(java.util.List<java.lang.Object> l)
        Parses an equivalence 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.

      • parseImplication

        private RelationalFormula parseImplication​(java.util.List<java.lang.Object> l)
        Parses an implication 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.

      • parseDisjunction

        private RelationalFormula 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 RelationalFormula 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 RelationalFormula 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 RelationalFormula 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 - if parsing fails

      • 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.