Package org.svvrl.goal.core.logic

  • Interface Summary 
    Interface Description
    FormulaRewriter
    A FormulaRewriter can rewrite a formula into a simpler one.
    NegationNormalForm<L extends Logic>
    This interface defines logic fomrulae that have a negation normal form.
    PrenexNormalForm<L extends Logic>
    This interface defines logic fomrulae that have a prenex normal form.
  • Class Summary 
    Class Description
    FormulaHolder<T extends Logic>
    A FormulaHolder holds a string that is supposed to be a formula of some logic.
    FormulaParser<T extends Logic>
    A FormulaParser object can parse a string into a formula of some logic.
    FormulaRewriterRepository
    FormulaRewriterRepository contains several registered formula rewriter.
    Literal
    A literal can be a proposition or the negation of a proposition.
    Logic  
    LogicSimplifier
    This class provides methods for simplify a logic formula based on formulae rewriters.
    LogicUnifier<T>
    This class provides some methods for the unification between two logic formulae.
    Proposition
    This is a class for propositions.
    Satisfiability
    This class provides methods for checking the satisfiability of an algebraic expression or a logic formula.
    Satisfiability.Result
    This class defines the result of a satisfiability test.
    Validity
    This class provides methods for checking the validity of an algebraic expression or a logic formula.
    Validity.Result
    This class defines the result of a validity test.
  • Exception Summary 
    Exception Description
    ParseException
    This exception is thrown if there is an error in parsing a formula.
    UnificationException
    A UnificationException indicates that the unification failed.