(=>
(and
(instance ?C ComputerBackingUp)
(dataProcessed ?C ?DD)
(instance ?DD DigitalData)
(agent ?C ?A))
(desires ?A
(exists (?T)
(and
(earlier
(WhenFn ?C) ?T)
(holdsDuring ?T
(exists (?PROC)
(and
(instance ?PROC ComputerProcess)
(capability ?PROC dataProcessed ?DD)))))))) |
ComputingBrands.kif 3403-3417 |
If X is an instance of backup, Y is processed by X, Y is an instance of digital data, and Z is an agent of X, then Z desires there exists W such that the time of existence of X happens earlier than W, there exists V such that V is an instance of computer process, and Y is capable of doing V as a data processed holds during W |
(=>
(and
(instance ?I SoftwareInstallation)
(dataProcessed ?I ?P)
(instance ?P ComputerProgram)
(destination ?I ?C))
(hasPurpose ?I
(exists (?PROC)
(computerRunning ?PROC ?C)))) |
ComputingBrands.kif 3499-3507 |
If X is an instance of install, Y is processed by X, Y is an instance of computer program, and X ends up at Z, then X has the purpose there exists W such that W is running on Z |
(=>
(and
(instance ?U SoftwareUnInstallation)
(equal ?T2
(WhenFn ?U))
(dataProcessed ?U ?P)
(instance ?P ComputerProgram)
(located ?U ?C))
(exists (?I ?T1)
(and
(instance ?I SoftwareInstallation)
(equal ?T1
(WhenFn ?I))
(dataProcessed ?I ?P)
(instance ?P ComputerProgram)
(located ?I ?C)
(earlier ?T1 ?T2)))) |
ComputingBrands.kif 3509-3523 |
If X is an instance of uninstall, equal Y and the time of existence of X, Z is processed by X, Z is an instance of computer program, and X is located at W, then All of the following hold: (1) there exist V (2) U such that V is an instance of install (3) equal U (4) the time of existence of V (5) Z is processed by V (6) Z is an instance of computer program (7) V is located at W (8) U happens earlier than Y |
(=>
(and
(processAborted ?Abort ?Process)
(dataProcessed ?Process ?Data))
(not
(exists (?Save)
(and
(instance ?Save DataSaving)
(dataProcessed ?Save ?Data))))) |
QoSontology.kif 2017-2025 |
If X is a process aborted of Y and Z is processed by X, then there doesn't exist W such that W is an instance of data saving and Z is processed by W |
(=>
(and
(instance ?Compression DataCompression)
(dataProcessed ?Compression ?Data)
(holdsDuring
(ImmediatePastFn
(WhenFn ?Compression))
(memorySize ?Data
(MeasureFn ?Memory ?Measure)))
(holdsDuring
(ImmediateFutureFn
(WhenFn ?Compression))
(memorySize ?Data
(MeasureFn ?NewMemory ?Measure))))
(lessThan ?NewMemory ?Memory)) |
QoSontology.kif 2050-2064 |
If X is an instance of data compression, Y is processed by X, Y requires Z W(s) holds during immediately before the time of existence of X, and Y requires V W(s) holds during immediately after the time of existence of X, then V is less than Z |
