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