public class ImplicationInfo extends DBInfo
Note: in theory we support several implication operators for one type. But it wasn't tested.
Modifier and Type | Class and Description |
---|---|
static class |
ImplicationInfo.ExtractImplResult |
Constructor and Description |
---|
ImplicationInfo(EquivalenceInfo eqInfo,
java.util.List<Assrt> assrtList,
TrOutput output,
boolean dbg) |
Modifier and Type | Method and Description |
---|---|
ProofStepStmt |
applyDisrtibutiveRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt hyp) |
GenProofStepStmt |
applyHyp(mmj.transforms.WorksheetInfo info,
GenProofStepStmt hypGenStep,
ParseNode stepNode,
Assrt assrt)
Apply implication rule (one or another pattern depend on hypothesis
form):
|
ProofStepStmt |
applyImplicationRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt min,
ParseNode implNode,
Assrt majAssrt)
Apply implication rule: like A & A -> B => B.
|
ProofStepStmt |
applyImplicationRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt min,
ProofStepStmt maj,
Stmt op)
Apply implication rule: like A & A -> B => B.
|
ProofStepStmt |
applyStubRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt core)
Apply stub implication rule: like B => A -> B.
|
ProofStepStmt |
applyTransitiveRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt min,
ParseNode implNode,
Assrt majAssrt)
Apply implication rule: like A -> B & B -> C => A -> C.
|
ImplicationInfo.ExtractImplResult |
extractPrefixAndGetImplPart(mmj.transforms.WorksheetInfo info) |
void |
finishStubRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt core)
Finish stub implication rule: like B => A -> B.
|
void |
finishTransitiveRule(mmj.transforms.WorksheetInfo info,
ProofStepStmt min,
ParseNode implNode,
Assrt majAssrt)
Finish implication rule: like A -> B & B -> C => A -> C.
|
void |
finishWithImplication(mmj.transforms.WorksheetInfo info,
ProofStepStmt min,
ParseNode implNode,
Assrt majAssrt)
Completes implication derivation step with input hypotheses.
|
Assrt |
getEqImplication(Cnst type) |
java.util.Collection<Stmt> |
getImplForPrefixOperators() |
Assrt |
getStubImplication(Stmt implOp) |
boolean |
isImplForPrefixOperator(Stmt op) |
boolean |
isImplOperator(Stmt op) |
public ImplicationInfo(EquivalenceInfo eqInfo, java.util.List<Assrt> assrtList, TrOutput output, boolean dbg)
public ProofStepStmt applyTransitiveRule(mmj.transforms.WorksheetInfo info, ProofStepStmt min, ParseNode implNode, Assrt majAssrt)
info
- the work sheet infomin
- the precondition (in the example it is statement A -> B)implNode
- the implication part (in the example it is node C)majAssrt
- the assert to construct B -> C steppublic void finishTransitiveRule(mmj.transforms.WorksheetInfo info, ProofStepStmt min, ParseNode implNode, Assrt majAssrt)
info
- the work sheet infomin
- the precondition (in the example it is statement A -> B)implNode
- the implication part (in the example it is node C)majAssrt
- the assert to construct B -> C steppublic ProofStepStmt applyStubRule(mmj.transforms.WorksheetInfo info, ProofStepStmt core)
info
- the work sheet infocore
- the hypothesis (B in the example)public void finishStubRule(mmj.transforms.WorksheetInfo info, ProofStepStmt core)
info
- the work sheet infocore
- the hypothesis (B in the example)public ProofStepStmt applyImplicationRule(mmj.transforms.WorksheetInfo info, ProofStepStmt min, ProofStepStmt maj, Stmt op)
info
- the work sheet infomin
- the precondition (in the example it is statement A)maj
- the implication (in the example it is statement A -> B)op
- implication operator (in the example it is ->)public ProofStepStmt applyImplicationRule(mmj.transforms.WorksheetInfo info, ProofStepStmt min, ParseNode implNode, Assrt majAssrt)
info
- the work sheet infomin
- the precondition (in the example it is statement A)implNode
- the implication part (in the example it is node B)majAssrt
- the assert to construct A -> B steppublic void finishWithImplication(mmj.transforms.WorksheetInfo info, ProofStepStmt min, ParseNode implNode, Assrt majAssrt)
info
- the work sheet infomin
- the precondition (in the example it is statement A)implNode
- the implication part (in the example it is node B)majAssrt
- the assert to construct A -> B steppublic ImplicationInfo.ExtractImplResult extractPrefixAndGetImplPart(mmj.transforms.WorksheetInfo info)
info
- the work sheet infopublic GenProofStepStmt applyHyp(mmj.transforms.WorksheetInfo info, GenProofStepStmt hypGenStep, ParseNode stepNode, Assrt assrt)
A -> B & B -> C => A -> C.
B & B -> C => C.
info
- the work sheet infohypGenStep
- the hypothesis (in the example it is B or "A -> B")stepNode
- the result node (in the example it is C)assrt
- the assertion to construct B -> C steppublic ProofStepStmt applyDisrtibutiveRule(mmj.transforms.WorksheetInfo info, ProofStepStmt hyp)
public boolean isImplOperator(Stmt op)
public boolean isImplForPrefixOperator(Stmt op)
public java.util.Collection<Stmt> getImplForPrefixOperators()