consequent

(=>     (instance ?Option Option)     (exists (?Type ?Date ?Stock ?Price)         (and             (or                 (equal ?Type CallOption)                 (equal ?Type PutOption))             (property ?Option ?Type)             (agreementExpirationDate ?Option ?Date)             (strikePrice ?Option ?Price)             (underlier ?Option ?Stock)             (measure ?Stock                 (MeasureFn 100 ShareUnit)))))	FinancialOntology.kif 2579-2590	If X is an instance of option, then there exist Y, Z,, , W and V such that equal Y and call option or equal Y and put option and X the attribute Y and X has expiration Z and V is a strike price of X and W is an underlier of X and the measure of W is 100 share unit(s)
(=>     (instance ?Spread ButterflySpread)     (exists (?Call1 ?Call2 ?Call3 ?Call4 ?Price1 ?Price2 ?Price3 ?Price4 ?U)         (and             (instance ?Call1 CallOption)             (instance ?Call2 CallOption)             (instance ?Call3 CallOption)             (instance ?Call4 CallOption)             (subProcess ?Call1 ?Spread)             (subProcess ?Call2 ?Spread)             (subProcess ?Call3 ?Spread)             (subProcess ?Call4 ?Spread)             (instance ?U UnitOfCurrency)             (strikePrice ?Call1                 (MeasureFn ?Price1 ?U))             (strikePrice ?Call2                 (MeasureFn ?Price2 ?U))             (strikePrice ?Call3                 (MeasureFn ?Price3 ?U))             (strikePrice ?Call4                 (MeasureFn ?Price4 ?U))             (lessThan ?Price1 ?Price2)             (lessThan ?Price1 ?Price3)             (greaterThan ?Price4 ?Price2)             (greaterThan ?Price4 ?Price2))))	FinancialOntology.kif 3176-3200	If X is an instance of butterfly spread, then there exist Y, Z,, , W,, , V,, , U,, , T,, , S,, , R and Q such that Y is an instance of call option and Z is an instance of call option and W is an instance of call option and V is an instance of call option and Y is a subprocess of X and Z is a subprocess of X and W is a subprocess of X and V is a subprocess of X and Q is an instance of unit of currency and U Q(s) is a strike price of Y and T Q(s) is a strike price of Z and S Q(s) is a strike price of W and R Q(s) is a strike price of V and U is less than T and U is less than S and R is greater than T and R is greater than T
(=>     (instance ?Straddle Straddle)     (exists (?Call ?Price ?Date ?Number ?Put)         (and             (equal                 (CardinalityFn                     (KappaFn ?Call                         (and                             (instance ?Call CallOption)                             (part ?Call ?Straddle)))) ?Number)             (equal                 (CardinalityFn                     (KappaFn ?Put                         (and                             (instance ?Put PutOption)                             (part ?Put ?Straddle)))) ?Number)             (forall (?Option)                 (=>                     (and                         (instance ?Option Option)                         (part ?Option ?Straddle))                     (and                         (agreementExpirationDate ?Option ?Date)                         (strikePrice ?Option ?Price)))))))	FinancialOntology.kif 3206-3230	If X is an instance of straddle, then All of the following hold: (1) there exist Y, Z,, , W,, , V (2) U such that equal the number of instances in the class described by Y (3) V (4) equal the number of instances in the class described by U (5) V (6) T T is an instance of option (7) T is a part of XT has expiration W (8) Z is a strike price of T

Show simplified definition (without tree view)
Show simplified definition (with tree view)