Success

The Success Ontology

The Success ontology has thee subontologies:

• The semantic success subontology is the original success ontology, designed for setting the status of problems, and the reporting the results of reasoning. The semantic success ontology assumes that the input is a 2-tuple of the form <Ax,C>, where Ax is a set (conjunction) of axioms and C is a set (conjunction) of conjectures. This is a common standard usage of ATP systems (often there is only a single conjecture). If the input does not have any conjectures, e.g., a set of axioms, then the set (conjunction) of formulae are used to form C and the 2-tuple is <TRUE,C>. The ontology values are based on the possible relationships between the sets of models of Ax and C.

• The type checking success subontology is designed to specify the results of type checking in typed logics.

• The verification success subontology is designed to specify the results of proof and model verification.

• Success (SUC):
  The logical data has been processed successfully.

• SemanticSuccess (SSU):
  The logical data has been reasoned about successfully.

  • UnsatisfiabilityPreserving (UNP):
    If there does not exist a model of Ax then there does not exist a model of C, i.e., if Ax is unsatisfiable then C is unsatisfiable.

  • SatisfiabilityPreserving (SAP):
    If there exists a model of Ax then there exists a model of C, i.e., if Ax is satisfiable then C is satisfiable.

  • TautologyPreserving (TAP):
    If every interpretation is a model of Ax then every interpretation is a model of C, i.e., if Ax is a tautology then C is a tautology.

  • EquiSatisfiable (ESA):
    There exists a model of Ax iff there exists a model of C, i.e., Ax is (un)satisfiable iff C is (un)satisfiable.

  • EquiTautologous (ETA):
    Every interpretation is a model of Ax iff every interpretation is a model of C, i.e., Ax is a tautology iff C is a tautology.

  • ModelExtending (MEX): C is over a conservative extension of the signature of Ax, e.g., due to Skolemization. 

Some interpretations are models Ax, some interpretations are models of C, and all models of C are conservative extensions of models of Ax (which also means that all models of C are models of Ax over the signature of C).

• • Satisfiable (SAT):
    Some interpretations are models of Ax, and some models of Ax are models of C.

  • FinitelySatisfiable (FSA):
    Some finite interpretations are finite models of Ax, and some finite models of Ax are finite models of C.

  • FiniteTheorem (FTH):
    All finite models of Ax are finite models of C.

  • Theorem (THM):
    All models of Ax are models of C.

  • SatisfiableAxiomsTheorem (STH):
    Some interpretations are models of Ax, and all models of Ax are models of C.

  • Equivalent (EQV):
    Some interpretations are models of Ax, all models of Ax are models of C, and all models of C are models of Ax.

  • TautologousConclusion (TAC):
    Some interpretations are models of Ax, and all interpretations are models of C.

  • WeakerConclusion (WEC):
    Some interpretations are models of Ax, all models of Ax are models of C, and some models of C are not models of Ax.

  • EquivalentTheorem (ETH):
    Some, but not all, interpretations are models of Ax, all models of Ax are models of C, and all models of C are models of Ax.

  • Tautology (TAU):
    All interpretations are models of Ax, and all interpretations are models of C.

  • WeakerTautologousConclusion (WTC):
    Some, but not all, interpretations are models of Ax, and all interpretations are models of C.

  • WeakerTheorem (WTH):
    Some interpretations are models of Ax, all models of Ax are models of C, some models of C are not models of Ax, and some interpretations are not models of C.

  • FiniteTautology (FTT):
    All finite interpretations are models of Ax, and all finite interpretations are models of C.

  • CounterUnsatisfiabilityPreserving (CUP):
    If there does not exist a model of Ax then there does not exist a model of ~C, i.e., if Ax is unsatisfiable then ~C is unsatisfiable.

  • CounterSatisfiabilityPreserving (CSP):
    If there exists a model of Ax then there exists a model of ~C, i.e., if Ax is satisfiable then ~C is satisfiable.

  • CounterTautologyPreserving (CTP):
    If every interpretation is a model of Ax then every interpretations is a model of ~C, i.e., if Ax is a tautology then ~C is a tautology.

  • EquiCounterSatisfiable (ECS):
    There exists a model of Ax iff there exists a model of ~C, i.e., Ax is (un)satisfiable iff ~C is (un)satisfiable.

  • EquiCounterTautologous (ECA):
    Every interpretation is a model of Ax iff every interpretation is a model of ~C, i.e., Ax a tautology iff ~C is a tautology.

  • CounterModelExtending (CMX):

Some interpretations are models Ax, some interpretations are models of ~C, and all models of ~C are conservative extensions of models of Ax (which also means that all models of ~C are models of Ax over the signature of C).

• • CounterSatisfiable (CSA):
    Some interpretations are models of Ax, and some models of Ax are models of ~C.

  • FinitelyCounterSatisfiable (FCS):
    Some finite interpretations are finite models of Ax, and some finite models of Ax are finite models of ~C.

  • FiniteCounterTheorem (FCT):
    All finite models of Ax are finite models of ~C.

  • CounterTheorem (CTH):
    All models of Ax are models of ~C.

  • SatisfiableAxiomsCounterTheorem (SCT):
    Some interpretations are models of Ax, and all models of Ax are models of ~C.

  • CounterEquivalent (CEQ):
    Some interpretations are models of Ax, all models of Ax are models of ~C, and all models of ~C are models of Ax, i.e., all interpretations are models of Ax xor of C.

  • UnsatisfiableConclusion (UNC):
    Some interpretations are models of Ax, and all interpretations are models of ~C, i.e., no interpretations are models of C.

  • WeakerCounterConclusion (WCC):
    Some interpretations are models of Ax, and all models of Ax are models of ~C, and some models of ~C are not models of Ax.

  • EquivalentCounterTheorem (ECT):
    Some, but not all, interpretations are models of Ax, all models of Ax are models of ~C, and all models of ~C are models of Ax.

  • Unsatisfiable (UNS):
    All interpretations are models of Ax, and all interpretations are models of ~C, i.e., no interpretations are models of C.

  • WeakerUnsatisfiableConclusion (WUC):
    Some, but not all, interpretations are models of Ax, and all interpretations are models of ~C.

  • WeakerCounterTheorem (WCT):
    Some interpretations are models of Ax, all models of Ax are models of ~C, some models of ~C are not models of Ax, and some interpretations are not models of ~C, i.e., some interpretations are models of C.

  • FinitelyUnsatisfiable (FUN):
    All finite interpretations are models of Ax, and all finite interpretations are models of ~C, i.e., no finite interpretations are models of C.

  • ContradictoryAxioms (CAX):
    No interpretations are models of Ax.

  • SatisfiableConclusionContradictoryAxioms (SCA):
    No interpretations are models of Ax, and some interpretations are models of C.

  • SatisfiableCounterConclusionContradictoryAxioms (SCC):
    No interpretations are models of Ax, and some interpretations are models of ~C.

  • TautologousConclusionContradictoryAxioms (TCA):
    No interpretations are models of Ax, and all interpretations are models of C.

  • WeakerConclusionContradictoryAxioms (WCA):
    No interpretations are models of Ax, and some, but not all, interpretations are models of C.

  • UnsatisfiableConclusionContradictoryAxioms (UCA):
    No interpretations are models of Ax, and all interpretations are models of ~C, i.e., no interpretations are models of C.

  • NoConsequence (NOC):
    Some interpretations are models of Ax, some models of Ax are models of C, and some models of Ax are models of ~C.

• TypeCheckSuccess (TSU):
  The logical data has been typed checked successfully.

  • TypeCheckPartial (TCP):
    Everything passed type checking, but some of the checking was partial, i.e., some things that passed might not be type correct.

  • TypeCheckedComplete (TCC):
    Everything passed type checking.

• VerifySuccess (VSU):
  The logical solution has been verified successfully.

  • VerifiedGood (VSG):
    The solution has been verified as good.

  • VerifiedBad (VSB):
    The solution has been verified as bad.