orbital.moon.logic.resolution
Class DefaultClausalFactory

java.lang.Object
  orbital.moon.logic.resolution.DefaultClausalFactory

All Implemented Interfaces:

ClausalFactory

public class DefaultClausalFactory
extends java.lang.Object
implements ClausalFactory

Factory for clauses and clausalsets.

Author:

André Platzer

See Also:

Abstract Factory

Constructor Summary

DefaultClausalFactory()

Method Summary

ClausalSet	asClausalSet(Formula f) 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.
void	setVerbose(boolean newVerbose) Add verbosity, i.e.

Methods inherited from class java.lang.Object

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

Constructor Detail

DefaultClausalFactory

public DefaultClausalFactory()

Method Detail

setVerbose

public void setVerbose(boolean newVerbose)

Add verbosity, i.e. print out a proof tree.

newClause

public Clause newClause()

Description copied from interface: ClausalFactory

Instantiates a new clause.

Specified by:

newClause in interface ClausalFactory

Returns:

a new (yet empty) clause.

See Also:

Factory Method

createClause

public Clause createClause(java.util.Set literals)

Description copied from interface: ClausalFactory

Instantiates a new clause.

Specified by:

createClause in interface ClausalFactory

Parameters:

literals - the set of literals for the new clause.

Returns:

a new clause, with the specified literals.

See Also:

Factory Method

newClausalSet

public ClausalSet newClausalSet()

Description copied from interface: ClausalFactory

Instantiates a new clausal set.

Specified by:

newClausalSet in interface ClausalFactory

Returns:

a new (yet empty) clausal set.

See Also:

Factory Method

createClausalSet

public ClausalSet createClausalSet(java.util.Set clauses)

Description copied from interface: ClausalFactory

Instantiates a new clausal set.

Specified by:

createClausalSet in interface ClausalFactory

Parameters:

clauses - the set of clauses for the new clausal set.

Returns:

a new clause, with the specified clauses.

See Also:

Factory Method

asClausalSet

public ClausalSet asClausalSet(Formula f)

Description copied from interface: ClausalFactory

Returns a clausal set representation of the given formula.

Converts the given formula to CNF in clausal set representation.

Specified by:

asClausalSet in interface ClausalFactory

See Also:

ClassicalLogic.Utilities.clausalForm(Formula,boolean)