Class Conjecture

java.lang.Object
  |
  +--Clause
        |
        +--Conjecture

public class Conjecture

extends Clause

This class implements a conjecture.

Author:

P. URSO

See Also:

EqualList

Fields inherited from class Clause

conj, disj, HYPOTHESE_NUM, LEMMA_NUM

Constructor Summary

protected	Conjecture(Equality e) Constructor of a conjecture.
	Conjecture(EqualList conj, EqualList disj) Constructor of a conjecture.

Method Summary

Conjecture	applySubst(Substitution sigma) Applies a substitution map to this conjecture
boolean	canUse(SpecialClause r) Tests if a specified rule could be used to simplify this conjecture.
boolean	getsIn(EqualList list) Tests if the conjecture gets a specified list of equalities in its conditions.
Hypothese	hypothese() Returns hypothese of the conjecture.
List	inductionVariables() Returns the list of induction variable of this conjecture.
boolean	isNFEqual(RuleTable rules) Tests if this conjecture is an equality that normal form
boolean	isTotology() Tests if this conjecture is a totology.
Conjecture	simplify(RuleTable rules) Applies a rewrite step on this conjecture.
String	toStringN() Returns a string representation of this clause with axiom number.

Methods inherited from class Clause

body, conditions, emptyBody, equals, num, oriented, prefix, semiOriented, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

Conjecture

public Conjecture(EqualList conj,
                  EqualList disj)

Constructor of a conjecture.

Parameters:

conj - conjonction part of the clause.

disj - disjonction part of the clause.

Conjecture

protected Conjecture(Equality e)

Constructor of a conjecture.

Parameters:

e - the only equality of the clause.

Method Detail

hypothese

public Hypothese hypothese()

Returns hypothese of the conjecture.

getsIn

public boolean getsIn(EqualList list)

Tests if the conjecture gets a specified list of equalities in its conditions.

Parameters:

list - the list of equalities.

Returns:

true if all equalities of list appear either in conjonction part - or toggled in disjonction part - of this conjecture.

applySubst

public Conjecture applySubst(Substitution sigma)

Applies a substitution map to this conjecture

Parameters:

sigma - the substitution.

Returns:

a new clause where all the occurrences of origin variables are substitued by theirs images.

isTotology

public boolean isTotology()

Tests if this conjecture is a totology. A clause is a totology either, if one of the equalities in the body is a syntaxic equality, or if the body and the conditions contain the same equality.

Returns:

true if any of theses cases.

canUse

public boolean canUse(SpecialClause r)

Tests if a specified rule could be used to simplify this conjecture.

Returns:

false if the clause appears in fathers of this conjecture and if this conjecture has not be simplified.

simplify

public Conjecture simplify(RuleTable rules)

Applies a rewrite step on this conjecture. Tries to find in the rewrite rules the definition of functions apparing in the clause. Make one step to normal form.

Parameters:

rules - the table of rewrite rules.

Returns:

the conjecture simplified, null otherwise.

See Also:

RuleTable

inductionVariables

public List inductionVariables()

Returns the list of induction variable of this conjecture.

isNFEqual

public boolean isNFEqual(RuleTable rules)

Tests if this conjecture is an equality that normal form

Parameters:

rules - rewrite rules to apply. of both sides are equals.

Returns:

true if there is juste one equality of that type.

toStringN

public String toStringN()

Returns a string representation of this clause with axiom number. The string representation consists of two lists of equalities. The one before the imply sign " => " is a conjonction, and the one after is a disjonction.

Returns:

a string representation of this clause.

See Also:

EqualList.toString()