ListSumFn - Sigma Knowledge base Browser

Browsing Interface : Welcome guest : log in

[ Home | Graph | ] KB: Language:
Formal Language:

KB Term:			Term intersection

English Word:

Sigma KEE - ListSumFn

ListSumFn

appearance as argument number 1

(documentation ListSumFn EnglishLanguage "The sum of all the numbers in a List.")	Merge.kif 3240-3240
(domain ListSumFn 1 List)	Merge.kif 3238-3238	The number 1 argument of sum of elements is an instance of list
(instance ListSumFn UnaryFunction)	Merge.kif 3237-3237	Sum of elements is an instance of unary function
(range ListSumFn RealNumber)	Merge.kif 3239-3239	The range of sum of elements is an instance of real number

appearance as argument number 2

(format EnglishLanguage ListSumFn "the sum of %1")	Merge.kif 3241-3241
(termFormat EnglishLanguage ListSumFn "sum of elements")	Merge.kif 3242-3242

antecedent

(=> (and (equal ?A (ListSumFn ?L)) (equal 1 (ListLengthFn ?L))) (equal ?A (ListOrderFn ?L 1)))	Merge.kif 3250-3254	If a real number is equal to the sum of a list and 1 is equal to length of the list, then the real number is equal to 1th element of the list
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L)))))	Merge.kif 3256-3266	If a real number is equal to the sum of a list and length of the list is greater than 1, then the real number is equal to (the first of the list and the sum of the sub-list from 2 to length of the list of the list)

consequent

(=> (and (amount ?S ?CO (MeasureFn ?N ?U)) (instance ?SI ?S) (measure ?SI (MeasureFn ?N2 ?U)) (part ?SI ?CO)) (exists (?L) (and (inList (MeasureFn ?N2 ?U) ?L) (equal ?L (AmountsFn ?S ?CO ?U)) (equal ?N (ListSumFn ?L)))))	Merge.kif 7632-7647	If amount a kind of substance, a corpuscular object and a real number an unit of mass(s) and a kind of substanceI is an instance of the kind of substance and the measure of the kind of substanceI is the real number2 the unit of mass(s) and the kind of substanceI is a part of the corpuscular object, then there exists a list such that the real number2 the unit of mass(s) is a member of the list and the list is equal to Amounts fn the kind of substance, the corpuscular object and the unit of mass and the real number is equal to the sum of the list
(=> (and (equal ?A (AverageFn ?L)) (greaterThan (ListLengthFn ?L) 0)) (equal ?A (DivisionFn (ListSumFn ?L) (ListLengthFn ?L))))	Merge.kif 3275-3282	If a real number is equal to the average of the numbers in a list and length of the list is greater than 0, then the real number is equal to the sum of the list and length of the list
(=> (and (equal ?A (ListSumFn ?L)) (greaterThan (ListLengthFn ?L) 1)) (equal ?A (AdditionFn (FirstFn ?L) (ListSumFn (SubListFn 2 (ListLengthFn ?L) ?L)))))	Merge.kif 3256-3266	If a real number is equal to the sum of a list and length of the list is greater than 1, then the real number is equal to (the first of the list and the sum of the sub-list from 2 to length of the list of the list)
(=> (and (fleetDeadWeightTonnage ?FLEET (MeasureFn ?T LongTon)) (vesselDeadWeightTonnage ?VESSEL (MeasureFn ?X LongTon)) (member ?VESSEL ?FLEET)) (exists (?L) (and (instance ?L List) (inList ?X ?L) (equal ?T (ListSumFn ?L)))))	Transportation.kif 2738-2748	If a real number long ton(s) is a fleet dead weight tonnage of a collection and another real number long ton(s) is a vessel dead weight tonnage of a water vehicle and the water vehicle is a member of the collection, then there exists a list such that the list is an instance of list and the other real number is a member of the list and the real number is equal to the sum of the list
(=> (and (instance ?O Odometer) (instance ?V Vehicle) (part ?O ?V) (instance ?T Translocation) (instrument ?T ?V) (path ?T ?P) (distanceOnPath (MeasureFn ?D ?U) ?P) (instance ?U LengthMeasure)) (hasPurpose ?O (exists (?M ?L ?DIST ?U) (and (instance ?M Measuring) (instrument ?M ?O) (measurementReading ?O ?DIST) (inList ?D ?L) (holdsDuring (WhenFn (EndFn ?M)) (and (equal ?DIST (MeasureFn (ListSumFn ?L) ?U)) (not (attribute ?O ResetMeasuringDevice))))))))	Cars.kif 2970-2996	If an object is an instance of odometer and another object is an instance of vehicle and the object is a part of the other object and a motion is an instance of translocation and the other object is an instrument for the motion and a transitway is path along which the motion occurs and the distance of the transitway is a real number an unit of measure(s) and the unit of measure is an instance of length measure, then the object has the purpose there exist an entity, another entity,, , the real numberIST and the unit of measure such that the entity is an instance of measuring and the object is an instrument for the entity and the real numberIST is a measurement reading of the object and the real number is a member of the other entity and the real numberIST is equal to the sum of the other entity the unit of measure(s) and reset measuring device is not an attribute of the object holds during the time of existence of the end of the entity

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

Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners