Success Ontology Meanings

Success (SUC): The logical data has been processed successfully. UnsatisfiabilityPreserving (UNP): If there does not exist a model of Ax then there does not exist a model of C. SatisfiabilityPreserving (SAP): If there exists a model of Ax then there exists a model of C. EquiSatisfiable (ESA): There exists a model of Ax iff there exists a model 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. Theorem (THM): 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. ContradictoryAxioms (CAX): No interpretations are models of Ax. SatisfiableConclusionContradictoryAxioms (SCA): 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. CounterUnsatisfiabilityPreserving (CUP): If there does not exist a model of Ax then there does not exist a model of ¬C. CounterSatisfiabilityPreserving (CSP): If there exists a model of Ax then there exists a model of ¬C. EquiCounterSatisfiable (ECS): There exists a model of Ax iff there exists a model of ¬C. CounterSatisfiable (CSA): Some interpretations are models of Ax, and some models of Ax are models of ¬C. CounterTheorem (CTH): 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. 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. FinitelyUnsatisfiable (FUN): All finite interpretations are finite models of Ax, and all finite interpretations are finite models of ¬C. Unsatisfiable (UNS): All interpretations are models of Ax, and all 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. SatisfiableCounterConclusionContradictoryAxioms (SCC): No interpretations are models of Ax, and some interpretations are models of ¬C. UnsatisfiableConclusionContradictoryAxioms (UCA): No interpretations are models of Ax, and all 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.