Orbital library

orbital.moon.logic.resolution
Interface ClausalFactory

All Known Implementing Classes:
DefaultClausalFactory

public interface ClausalFactory

Factory for clauses and clausal sets.

Author:
André Platzer
See Also:
ResolutionBase.getClausalFactory(), DefaultClausalFactory, Abstract Factory

Method Summary
 ClausalSet asClausalSet(Formula formula)
          Returns a clausal set representation of the given formula.
 ClausalSet createClausalSet(java.util.Set clauses)
          Instantiates a new clausal set.
 Clause createClause(java.util.Set literals)
          Instantiates a new clause.
 ClausalSet newClausalSet()
          Instantiates a new clausal set.
 Clause newClause()
          Instantiates a new clause.
 

Method Detail

newClause

Clause newClause()
Instantiates a new clause.

Returns:
a new (yet empty) clause.
See Also:
Factory Method
Postconditions:
RES≠RES

createClause

Clause createClause(java.util.Set literals)
Instantiates a new clause.

Parameters:
literals - the set of literals for the new clause.
Returns:
a new clause, with the specified literals.
See Also:
Factory Method
Postconditions:
RES≠RES ∧ "RES=literals"

newClausalSet

ClausalSet newClausalSet()
Instantiates a new clausal set.

Returns:
a new (yet empty) clausal set.
See Also:
Factory Method
Postconditions:
RES≠RES

createClausalSet

ClausalSet createClausalSet(java.util.Set clauses)
Instantiates a new clausal set.

Parameters:
clauses - the set of clauses for the new clausal set.
Returns:
a new clause, with the specified clauses.
See Also:
Factory Method
Postconditions:
RES≠RES ∧ "RES=clauses"

asClausalSet

ClausalSet asClausalSet(Formula formula)
Returns a clausal set representation of the given formula.

Converts the given formula to CNF in clausal set representation.

See Also:
ClassicalLogic.Utilities.clausalForm(Formula,boolean)
Postconditions:
(RES.toFormula() <=> formula) ∧ RES in CNF

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.