    All Packages  Class Hierarchy  This Package  Previous  Next  Index

# Class JavaAgent.resource.fopl.Formula

    java.lang.Object
       |
       +----JavaAgent.resource.fopl.Formula

public abstract class Formula
extends Object
implements Parsable, KRSentence

A Formula is an abstraction. A Formula is usually used in logic to represent a proposition or sentence that is either true or false. Currently, there are several kinds of Formulae implemented.

See Also:
  Literal, NegFormula, MultiConFormula, BinConFormula, QuantFormula

##

Formula()

##

clone()
  This function generates a copy of this Formula.
clone(Substitution)
  Returns a copy of this Formula with Variables replaced according to the given Substitution.
equals(Object)
  This function tests whether this and the given Object are equal.
parse(InputStream)
  This function can be used to parse a given InputStream that represents a Formula.
parse(String)
  This function can be used to parse a given String that represents a Formula.
toSkolemizedAndOrForm()
  This function returns a new Formula which is the skolemized version of this Formula in which the only connectives are AND and OR and only literals may be negated.
toSkolemizedAndOrForm(Substitution, Vector, boolean)
  This function returns a new Formula which is the skolemized AND/OR form of this Formula.

##

Formula

     public Formula()

##

clone

     public abstract Object clone()

  This function generates a copy of this Formula. The copy will contain the same Variables and Symbols as the original.

  Returns:
    an equal copy of this Formula
  Overrides:
    clone in class Object

clone

     public abstract Formula clone(Substitution s) throws IllegalArgumentException

  Returns a copy of this Formula with Variables replaced according to the given Substitution. Symbols in the copy will be the same as the original ones but Variables will be repalced by the respective Terms in the given Substitution. A Variable not occurring in the Substitution will be replaced by a new (different) Variable with the same name. The given Substitution will be extended to include the mappings of old Variables to new ones.

  This function can also be used to generate a copy of this Formula that contains a new set of Variables. The given Substitution should be a new, empty Substitution in this case. Otherwise cloning can be seen as instantiating the Formula.

  Parameters:
    s - the Substitution that tells us how to replace Variables
  Returns:
    a new Formula that is an instance of this Formula; the Substitution `s` will be extended with any new Variable replacements introduced
  Throws: IllegalArgumentException
    An exception can occur if the given Substitution is null. In this case `clone()` (above) should be used.

toSkolemizedAndOrForm

     public Formula toSkolemizedAndOrForm()

  This function returns a new Formula which is the skolemized version of this Formula in which the only connectives are AND and OR and only literals may be negated. This is done by:
  1. adding information about Variable types in the quantfication to the Formula itself;
  2. replacing the connectives IMPLIES, IFF, and XOR by their equivalent combinations of AND and OR; this may lead to a multiplication of sub-formuae;
  3. pulling the negations into the Formula using mainly de Morgan's law; this may also reverse quantifiers;
  4. replacing Variables that are existentially quantified at this point by appropriate Skolem symbols and functions;
  5. dropping the quantifiers;

  Returns:
    a new Formula which is the skolemized AND/OR form of this Formula

toSkolemizedAndOrForm

     protected abstract Formula toSkolemizedAndOrForm(Substitution s,
                                                      Vector allQuantVars,
                                                      boolean isNegated) throws IllegalArgumentException

  This function returns a new Formula which is the skolemized AND/OR form of this Formula. The returned Substitution indicates how Variables are to be replaced; either by copies of the Variable or a Skolem symbol (ConstTerm) or function. The Variables to be replaced will still be in the Formula though! The given Vector of Variables is used to keep track of any Variables that are universally quantified at this point. Finally, the given boolean indicates whether the Formula is to be treated as negated at this point.

  Parameters:
    s - the Substitution that tells us how to replace Variables
    allQuantVars - the Vector of universally quantified Variables
    isNegated - whether the Formula is negated
  Returns:
    a new Formula (either a MultiConFormula or a Literal) which is the skolemized AND/OR form of this Formula; the Substitution `s` will be extended with any new Variable replacements introduced
  Throws: IllegalArgumentException
    An exception can occur if the given Substitution or Vector are null.

equals

     public abstract boolean equals(Object otherForm)

  This function tests whether this and the given Object are equal. In general, two Formulae are equal if they have the same structure and consist of the same Symbols and Variables. This is not a test for logical equivalence or unifyability!

  Parameters:
    otherForm - the Formula this one is to be compared to
  Returns:
    whether the given Object is equal to this one
  Overrides:
    equals in class Object

parse

     public static Formula parse(String s) throws IllegalArgumentException, ParseException

  This function can be used to parse a given String that represents a Formula. The syntax in BNF is as follows:

       <formula>    ::= ( <quant> <c-from> ) | <c-from>
       <quant>      ::= ( <quantifier> <varspec>+ )
       <quantifier> ::= forall | exists
       <varspec>    ::= <variable> |
                        ( <variable> <constant> )
       <c-from>     ::= <literal> |
                        ( not <formula> ) |
                        ( and <formula> <formula>+ ) |
                        ( or <formula> <formula>+ ) |
                        ( implies <formula> <formula> ) |
                        ( iff <formula> <formula> ) |
                        ( xor <formula> <formula> ) |
       <literal>    ::= <constant> |
                        ( = <term> <term> )
                        ( <constant> <term>+ )
       <term>       ::= <constant> | <variable> |
                        ( <constant> <term>+ ) |
       <variable>   ::= ?<name>
       <constant>   ::= <name>

  Throws: IllegalArgumentException
    An exception will occur if the supplied String is empty or null.
  Throws: ParseException
    An exception can occur if parsing failed. Potential reasons include a syntax error or an I/O problem.

parse

     public static Formula parse(InputStream ist) throws IllegalArgumentException, IOException, ParseException

  This function can be used to parse a given InputStream that represents a Formula. The syntax in BNF is as above except that the first token should be the word `FORMULA` so that the generic parser knows what it has to expect. This is added automatically when parsing a String.

  Throws: IllegalArgumentException
    An exception will occur if the supplied InputStream is null.
  Throws: IOException
    An exception can occur if there are problems reading from the given InputStream.
  Throws: ParseException
    An exception can occur if parsing failed. Potential reasons include a syntax error.

    All Packages  Class Hierarchy  This Package  Previous  Next  Index