public class EquivalenceInfo extends DBInfo
Note: Now there is a restriction: the library has to define only one equivalence operator for every type. In set.mm we have 2 types: wff, class.
Constructor and Description |
---|
EquivalenceInfo(java.util.List<Assrt> assrtList,
TrOutput output,
boolean dbg) |
Modifier and Type | Method and Description |
---|---|
ParseNode |
createEqNode(ParseNode left,
ParseNode right)
Creates equivalence node (e.g.
|
GenProofStepStmt |
createReverseStep(mmj.transforms.WorksheetInfo info,
GenProofStepStmt source)
Creates reverse step for another equivalence step (e.g.
|
void |
fillDeductRules(java.util.List<Assrt> assrtList,
ImplicationInfo implInfo) |
Stmt |
getEqStmt(Cnst type) |
GenProofStepStmt |
getTransitiveStep(mmj.transforms.WorksheetInfo info,
GenProofStepStmt first,
GenProofStepStmt second)
This function creates transitive inference for two steps (= is the
example of equivalence operator).
|
boolean |
isEquivalence(Stmt stmt) |
public void fillDeductRules(java.util.List<Assrt> assrtList, ImplicationInfo implInfo)
public ParseNode createEqNode(ParseNode left, ParseNode right)
left
- the left noderight
- the right nodepublic GenProofStepStmt createReverseStep(mmj.transforms.WorksheetInfo info, GenProofStepStmt source)
info
- the work sheet infosource
- the source (e.g. a = b)public GenProofStepStmt getTransitiveStep(mmj.transforms.WorksheetInfo info, GenProofStepStmt first, GenProofStepStmt second)
info
- the work sheet infofirst
- the first statement (e.g. a = b )second
- the second statement (e.g. b = c )public boolean isEquivalence(Stmt stmt)