edu.isi.powerloom.logic
Class Justification

java.lang.Object
  edu.isi.stella.Stella_Object
      edu.isi.stella.StandardObject
          edu.isi.powerloom.logic.Justification

Direct Known Subclasses:

ClashJustification, ForwardJustification, PrimitiveStrategy

public class Justification
extends StandardObject

Field Summary

Cons	antecedents Antecedents justifications of this justification.
Keyword	inferenceRule Keyword describing the inference rule used to conclude the proposition of this justification.
double	negativeScore Negative partial match score of the derived proposition.
Justification	patternJustification Backpointer to the closest parent :PATTERN justification containing the variable substitutions from the associated pattern control frame.
double	positiveScore Positive partial match score of the derived proposition.
Proposition	proposition The proposition supported by this justification.
boolean	reversePolarityP True if proposition was derived in reverse polarity.
KeyValueMap	substitution List of variable bindings recorded for :PATTERN justifications.
TruthValue	truthValue Truth value of the derived proposition.

Constructor Summary

Justification()

Method Summary

static Stella_Object	accessJustificationSlotValue(Justification self, Symbol slotname, Stella_Object value, boolean setvalueP)
static void	backlinkToPatternJustification(Justification justification, Justification pattern)
static boolean	betterWhynotProofP(Justification proof1, Justification proof2)
static void	collectFailedGoals(Justification proof, List failures)
static void	collectVisibleAntecedents(Justification self, List visibleantecedents)
static int	computeNumberOfFailedSubgoals(Justification proof)
static int	computeProofDeviation(Justification proof1, Justification proof2, int maxdeviations, KeyValueList deviations)
Cons	consify() Return a CONS tree representation of the proof self.
static Cons	consifyJustification(Justification self, Keyword style) Return a CONS tree representation of the proof self.
Justification	copy() Return a copy of the proof starting at self.
static boolean	cutoffGoalJustificationP(Justification self)
static ExplanationInfo	explanationInfo(Justification self, KeyValueList mapping)
static java.lang.String	explanationTruthMarker(Justification justification)
static boolean	failedGoalJustificationP(Justification self)
static ExplanationInfo	getExplanationInfo(Justification self, KeyValueList mapping, boolean createP)
static KeyValueMap	getExplanationSubstitution(Justification self)
Keyword	inferenceDirection()
Keyword	inferenceStrategy()
static boolean	justificationEqlP(Justification just1, Justification just2)
static java.lang.String	makeRuleOriginExplanationPhrase(Justification self)
static boolean	markAsCutoffGoalP(Justification self)
static boolean	markAsExplicitAssertionP(Justification self)
static boolean	markAsFailedGoalP(Justification self)
static Justification	newJustification()
static boolean	partiallyFollowsP(Justification self)
Surrogate	primaryType() Returns the primary type of self.
static KeyValueList	printExplanation(Justification self, OutputStream stream, KeyValueList mapping, int maxdepth, Keyword audience)
static void	printExplanationAntecedents(Justification self, OutputStream stream, KeyValueList mapping, int maxdepth, List unexplained)
static void	printExplanationHeader(Justification self, OutputStream stream, KeyValueList mapping)
static void	printExplanationSubstitution(Justification self, OutputStream stream, KeyValueList mapping)
static void	printExplanationSupport(Justification self, OutputStream stream, KeyValueList mapping, int maxdepth, List unexplained)
static void	printExplanationText(Justification self, OutputStream stream, KeyValueList mapping)
static void	printJustificationProposition(Justification self, OutputStream stream, int indent)
static void	printJustificationPropositionForFormat(Justification self, OutputStream stream, int indent)
static void	printOneExplanation(Justification self, OutputStream stream, KeyValueList mapping, int maxdepth, List unexplained)
static void	printWhynotJustification(Justification justification, OutputStream stream, int maxdepth, Keyword style, boolean summaryP) Print a WHYNOT justification to stream according to maxdepth and style.
static ExplanationInfo	registerJustification(Justification self, KeyValueList mapping)
static Cons	retrievalProofSolution(Justification proof, QueryIterator query)
static List	visibleAntecedents(Justification self)
static Justification	visibleJustification(Justification self)
static KeyValueMap	yieldJustificationSubstitution(Justification justification, KeyValueMap substitution, Proposition argument)

Methods inherited from class edu.isi.stella.StandardObject

arrayTypeSpecifierP, baseTypeToTypeSpec, cantOverwriteActiveCollectionSlot, compatibleParameterTypesP, computeAnchoredTypeSpec, computeRelativeTypeSpec, conformingTypeSpecP, copyWrappedLiteral, cppNonPointerTypeP, cppReferenceTypeP, cppReferencizeType, cppTranslateAndPointerizeTypeSpec, cppTranslateAndReferencizeTypeSpec, cppTranslateTypeSpec, cppTypeWithoutInteriorPointersP, dropSlotValue, extractParameterType, extractRequiredArgumentValues, getSlot, hashCode_, idlTranslateTypeSpec, inverseSlotDemon, javaLiteralP, javaNativeLiteralWrapperNames, javaSpecialSetterName, javaTranslateArrayOfTypeSpec, javaTranslateTypeSpec, javaTranslateTypeSpecForFunction, javaTranslateTypeSpecHelper, javaYieldClassObjectArrayExpression, javaYieldClassObjectExpression, javaYieldFullyQualifiedTypeName, javaYieldTranslatedClassAndMethodNames, listifyTypeSpec, lookupClTypeFromStellaType, objectEqlP, putSlotValue, readSlotValue, runConstructorDemons, runDestructorDemons, runSlotDemons, runSlotGuardDemonsP, standardObjectP, subTypeSpecOfP, twoArgumentLeastCommonSupertype, typeSpecToBaseType, typeSpecToClass, typeToWalkedNullValueTree, validateTypeSpecifier, voidP, walkTypeSpecIsNativeTypeP, writeSlotValue, yieldTypeSpecTree

Methods inherited from class edu.isi.stella.Stella_Object

_, accessInContext, addPropertyValue, amPm, anchoredTypeSpecifierP, andOrNotTreeP, applyCoercionMethod, atomicExpressionP, bindToSurrogateP, booleanP, bootstrapIsaP, bquotify, cast, characterP, chooseSortPredicate, clConditionalizeTypeDeclarationTree, clTranslateAtomicTree, clTranslateATree, clTranslateBooleanTest, clTranslatePlainBooleanTest, clTranslateVerbatimBodySymbols, clYieldTypedExpressionTree, coerceATree, coerceEvaluatedTree, coerceMvTree, coerceOptionValue, coerceToBoolean, coerceToFloat, coerceToHashSet, coerceToModule, coerceToModuleName, coerceToString, coerceToSymbol, coerceToXmlElement, coerceValueToBoolean, coerceValueToFloat, coerceValueToString, coerceValueToType, coercibleP, collectFeatureList, collectKeyValueList, commonLispSymbolP, computeExpressionType, consifyListsAndIterators, consP, consTreeMatchP, convertToLiteral, copyConsTree, cppArgumentIsStreamP, cppBinaryOperatorP, cppBlockP, cppMaybeOutputStatementWithParentheses, cppOperatorP, cppOutputAtomicExpression, cppOutputLiteral, cppOutputOneActualParameter, cppOutputStatement, cppOutputTypedEntity, cppPrognifyStatement, cppPrognP, cppStatementToList, cppStreamIsStandardOutputP, cpptrans, cppTranslateAtomicTree, cppTranslateATree, cppTranslatedArrayTypeP, csValueP, dateDivider, dateTimeDivider, day, dealWithAmPm, dealWithEra, dealWithNoonMidn, decrementReferenceCount, defaultOptionHandler, defineSystem, defmodule, deletedP, describe, describeObject, describeTersely, destructureMethodNameTree, deUglifyParseTree, either, eqlP, eqlToBooleanP, eqlToCharacterP, eqlToFloatP, eqlToIntegerP, eqlToLongIntegerP, eqlToStringP, equalConsTreesP, equalHashCode, equalP, era, estimatedEvaluationCost, evaluate, evaluateArgumentTree, evaluateAtomicTree, evaluateCommand, expandBquoteTree, filterModuleP, floatP, free, get, getObject, getProperty, hashlist, hashMemoizedArguments, helpBquotify, helpClTranslateATree, helpCoerceATree, helpLptrans, helpPrintOutline, helpTransformBooleanProceduralExpression, helpWalkATree, homeModule, hour, idlOutputAtomicExpression, idlOutputLiteral, idlOutputStatement, idlTranslateAtomicTree, idlTranslateATree, illegalTreeP, implodePathname, incrementallyTranslate, incrementReferenceCount, inlineUnwrapBoolean, inlineWrapBoolean, inModule, integerP, isaP, javaBinaryOperatorP, javaBlockP, javaEndOfLineTokenP, javaHelpOutputPrintStream, javaMaybeOutputStatementWithParentheses, javaOperatorP, javaOutputLiteral, javaOutputStatement, javaPrognP, javaStreamIsStandardOutputP, javaSymbolCaseP, javaTranslateAtomicTree, javaTranslateATree, javaTranslateWithNativeWrapper, jptrans, keywordP, legalTokenizerFromStateP, legalTokenizerStateP, legalTokenizerToStateP, literalEqlP, logLevelLE, longIntegerP, lptrans, makeEvaluatableBquoteTree, makeFileNameFromRelativePath, makeMemoizedValueEntry, makeMemoizedValueEntryn, matchConsTree, methodSlotP, minute, month, nameToString, nilP, noonMidn, numberWrapperToFloat, objectEqualP, objectHashCode, one, oneI, onlyIf, parametricTypeSpecifierP, parseArrayDimensionsSpec, parseOptions, parseTokenizerCharacterSpec, parseTokenizerStateModifiers, permanentCopy, permanentify, permanentifyForm, po, prettyPrintLiteral, primaryClass, printObject, printOutline, printStellaCode, printStellaDefinition, printUndefinedSuperClasses, proceduralExpressionP, ptrans, publicSlots, registerRecycledItem, runOptionHandlerP, safeEqualHashCode, safeHashCode, safePrimaryType, safeYieldTypeSpecifier, searchConsTreeP, searchConsTreeWithFilterP, searchForObject, secondp, setProperty, sideEffectFreeExpressionP, simplifyBquoteTree, specialp, stella_Increment, stellaClassP, stellaCollectionP, stellaNeedToCompileP, stellaNeedToTranslateP, stellaObjectP, stellify, storageSlotP, stringifyInModule, stringP, substituteConsTree, substituteOnce, surrogateP, surrogatify, sweep, symbolCaseP, symbolP, sysTree, targetLanguageType, taxonomyIsaP, timeDivider, timeMultiply, tokenizerIncludeSpecP, tokenizerToStateAlias, tokenizerToStateName, toString, traceIf, traceKeywordP, transientifyForm, transientObjectP, transientSymbolP, translateWalkedTree, treeSize, treeToTrees, trueOptionP, tryToEvaluate, typeP, typify, unmake, unregisterRecycledItem, updateInContext, valuesTreeP, variableExpressionP, verbatimStringP, verbatimTreeP, vetOptions, vrletExpressionP, walkAtomicTree, walkATree, walkCollectionTree, walkDontCallMeTree, walkedExpressionExpression, walkedExpressionType, walkExpressionTree, walkMvExpressionTree, walkMvTree, walkStatement, walkTopLevelExpression, walkWithoutTypeTree, warnAboutUnknownSourceType, weekday, withinContext, withinModule, withinWorld, withStellaTokenizer, withSystemDefinition, withTokenizer, wrapperP, wrapWhereTest, xmlAttributeP, xmlBaseAttributeP, xmlCdataFormP, xmlCdataP, xmlDeclarationFormP, xmlDeclarationP, xmlDoctypeFormP, xmlElementFormP, xmlElementP, xmlGlobalAttributeP, xmlLocalAttributeP, xmlnsAttributeP, xmlProcessingInstructionFormP, xmlProcessingInstructionP, xmlTagCase, year, yieldCondTest, yieldCondTestOrTests, yieldHardcodedCaseSymbolIdOrIds, yieldInCursorClausesForArgumentList, yieldInCursorClausesForGeneralCollection, yieldInCursorClausesForVector, yieldTypeSpecifier, zone, zoneMinute

Methods inherited from class java.lang.Object

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

Field Detail

inferenceRule

public Keyword inferenceRule

Keyword describing the inference rule used to conclude the proposition of this justification.

proposition

public Proposition proposition

The proposition supported by this justification.

antecedents

public Cons antecedents

Antecedents justifications of this justification.

patternJustification

public Justification patternJustification

Backpointer to the closest parent :PATTERN justification containing the variable substitutions from the associated pattern control frame. If this is a :PATTERN justification, the slot points to the parent pattern.

substitution

public KeyValueMap substitution

List of variable bindings recorded for :PATTERN justifications.

reversePolarityP

public boolean reversePolarityP

True if proposition was derived in reverse polarity.

truthValue

public TruthValue truthValue

Truth value of the derived proposition.

positiveScore

public double positiveScore

Positive partial match score of the derived proposition.

negativeScore

public double negativeScore

Negative partial match score of the derived proposition.

Constructor Detail

Justification

public Justification()

Method Detail

newJustification

public static Justification newJustification()

printWhynotJustification

public static void printWhynotJustification(Justification justification,
                                            OutputStream stream,
                                            int maxdepth,
                                            Keyword style,
                                            boolean summaryP)

Print a WHYNOT justification to stream according to maxdepth and style. Print a summary only if summaryP is TRUE.

Parameters:

justification -

stream -

maxdepth -

style -

summaryP -

collectFailedGoals

public static void collectFailedGoals(Justification proof,
                                      List failures)

retrievalProofSolution

public static Cons retrievalProofSolution(Justification proof,
                                          QueryIterator query)

computeProofDeviation

public static int computeProofDeviation(Justification proof1,
                                        Justification proof2,
                                        int maxdeviations,
                                        KeyValueList deviations)

betterWhynotProofP

public static boolean betterWhynotProofP(Justification proof1,
                                         Justification proof2)

computeNumberOfFailedSubgoals

public static int computeNumberOfFailedSubgoals(Justification proof)

collectVisibleAntecedents

public static void collectVisibleAntecedents(Justification self,
                                             List visibleantecedents)

visibleAntecedents

public static List visibleAntecedents(Justification self)

visibleJustification

public static Justification visibleJustification(Justification self)

printExplanationAntecedents

public static void printExplanationAntecedents(Justification self,
                                               OutputStream stream,
                                               KeyValueList mapping,
                                               int maxdepth,
                                               List unexplained)

printExplanationSubstitution

public static void printExplanationSubstitution(Justification self,
                                                OutputStream stream,
                                                KeyValueList mapping)

getExplanationSubstitution

public static KeyValueMap getExplanationSubstitution(Justification self)

makeRuleOriginExplanationPhrase

public static java.lang.String makeRuleOriginExplanationPhrase(Justification self)

partiallyFollowsP

public static boolean partiallyFollowsP(Justification self)

markAsCutoffGoalP

public static boolean markAsCutoffGoalP(Justification self)

markAsFailedGoalP

public static boolean markAsFailedGoalP(Justification self)

markAsExplicitAssertionP

public static boolean markAsExplicitAssertionP(Justification self)

printExplanationText

public static void printExplanationText(Justification self,
                                        OutputStream stream,
                                        KeyValueList mapping)

printExplanationHeader

public static void printExplanationHeader(Justification self,
                                          OutputStream stream,
                                          KeyValueList mapping)

printJustificationProposition

public static void printJustificationProposition(Justification self,
                                                 OutputStream stream,
                                                 int indent)

printJustificationPropositionForFormat

public static void printJustificationPropositionForFormat(Justification self,
                                                          OutputStream stream,
                                                          int indent)

printOneExplanation

public static void printOneExplanation(Justification self,
                                       OutputStream stream,
                                       KeyValueList mapping,
                                       int maxdepth,
                                       List unexplained)

printExplanationSupport

public static void printExplanationSupport(Justification self,
                                           OutputStream stream,
                                           KeyValueList mapping,
                                           int maxdepth,
                                           List unexplained)

printExplanation

public static KeyValueList printExplanation(Justification self,
                                            OutputStream stream,
                                            KeyValueList mapping,
                                            int maxdepth,
                                            Keyword audience)

explanationInfo

public static ExplanationInfo explanationInfo(Justification self,
                                              KeyValueList mapping)

getExplanationInfo

public static ExplanationInfo getExplanationInfo(Justification self,
                                                 KeyValueList mapping,
                                                 boolean createP)

registerJustification

public static ExplanationInfo registerJustification(Justification self,
                                                    KeyValueList mapping)

explanationTruthMarker

public static java.lang.String explanationTruthMarker(Justification justification)

consifyJustification

public static Cons consifyJustification(Justification self,
                                        Keyword style)

Return a CONS tree representation of the proof self. Each proof step is represented as a CONS tree of the form (<proposition> (<key> <value>...) <antecedent>...) where each <antecedent> is a CONS tree representing a subproof. style indicates what nodes in the proof tree should be suppressed. :RAW preserves the original structure literally, :VERBOSE keeps AND- introductions but suppresses all auxiliary (non-logical) nodes such as pattern nodes, and :BRIEF additionally suppresses AND-introduction nodes.

Parameters:

self -

style -

Returns:

Cons

consify

public Cons consify()

Return a CONS tree representation of the proof self. Each proof step is represented as a CONS tree of the form (<proposition> (<key> <value>...) <antecedent>...) where each <antecedent> is a CONS tree representing a subproof. The consification follows the original proof structure literally, i.e., no uninteresting nodes such as patterns or AND-introductions are suppressed.

Overrides:

consify in class Stella_Object

Returns:

Cons

cutoffGoalJustificationP

public static boolean cutoffGoalJustificationP(Justification self)

failedGoalJustificationP

public static boolean failedGoalJustificationP(Justification self)

backlinkToPatternJustification

public static void backlinkToPatternJustification(Justification justification,
                                                  Justification pattern)

copy

public Justification copy()

Return a copy of the proof starting at self. Allocates all new justification objects, but structure-shares other information such as propositions and substitutions.

Returns:

Justification

justificationEqlP

public static boolean justificationEqlP(Justification just1,
                                        Justification just2)

yieldJustificationSubstitution

public static KeyValueMap yieldJustificationSubstitution(Justification justification,
                                                         KeyValueMap substitution,
                                                         Proposition argument)

accessJustificationSlotValue

public static Stella_Object accessJustificationSlotValue(Justification self,
                                                         Symbol slotname,
                                                         Stella_Object value,
                                                         boolean setvalueP)

inferenceDirection

public Keyword inferenceDirection()

inferenceStrategy

public Keyword inferenceStrategy()

primaryType

public Surrogate primaryType()

Description copied from class: Stella_Object

Returns the primary type of self. Gets defined automatically for every non-abstract subclass of OBJECT.

Overrides:

primaryType in class Stella_Object

Returns:

Surrogate