TreeView Knowledge Base Browser - RemainderFn

Browsing Interface : Welcome guest : log in

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

KB Term:			Term intersection

English Word:

Sigma KEE - RemainderFn

RemainderFn

appearance as argument number 1

(documentation RemainderFn ChineseLanguage "(RemainderFn ?NUMBER ?DIVISOR)是数字 ?NUMBER 除以数字 ?DIVISOR 的余数，商数的正负值与 ?DIVISOR 相同。")	chinese_format.kif 2267-2268
(documentation RemainderFn EnglishLanguage "(RemainderFn ?NUMBER ?DIVISOR) is the remainder of the number ?NUMBER divided by the number ?DIVISOR. The result has the same sign as ?DIVISOR.")	Merge.kif 5004-5006
(domain RemainderFn 1 Integer)	Merge.kif 5000-5000	The number 1 argument of remainder is an instance of integer
(domain RemainderFn 2 Integer)	Merge.kif 5001-5001	The number 2 argument of remainder is an instance of integer
(instance RemainderFn BinaryFunction)	Merge.kif 4997-4997	Remainder is an instance of binary function
(instance RemainderFn PartialValuedRelation)	Merge.kif 4999-4999	Remainder is an instance of partial valued relation
(range RemainderFn Integer)	Merge.kif 5002-5002	The range of remainder is an instance of integer

appearance as argument number 2

(format ChineseLanguage RemainderFn "%1 模除 %2")	chinese_format.kif 722-722
(format EnglishLanguage RemainderFn "%1 mod %2")	english_format.kif 724-724
(termFormat ChineseLanguage RemainderFn "余函数")	chinese_format.kif 723-723
(termFormat ChineseLanguage RemainderFn "剩余")	domainEnglishFormat.kif 49425-49425
(termFormat ChineseTraditionalLanguage RemainderFn "剩餘")	domainEnglishFormat.kif 49424-49424
(termFormat EnglishLanguage RemainderFn "remainder")	domainEnglishFormat.kif 49423-49423

antecedent

(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1))	Merge.kif 5008-5019	If an integer mod another integer is equal to a third integer and the other integer is not equal to 0, then (the largest integer less than or equal to the integer and the other integer and the other integer and the third integer) is equal to the integer
(=> (and (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER) (not (equal ?NUMBER2 0))) (equal (SignumFn ?NUMBER2) (SignumFn ?NUMBER)))	Merge.kif 5034-5042	If an integer mod another integer is equal to a third integer and the other integer is not equal to 0, then the sign of the other integer is equal to the sign of the third integer

consequent

(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?NUMBER) 0))))	Merge.kif 4765-4776	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the other integer mod the integer is equal to 0
(=> (and (equal (GreatestCommonDivisorFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?GREATER) (and (greaterThan ?GREATER ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?ELEMENT ?GREATER) 0)))))))	Merge.kif 4778-4792	If the greatest common divisor of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is greater than the integer and for all a third integer if the third integer is a member of (@ROW), then the third integer mod the other integer is equal to 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?NUMBER ?ELEMENT) 0))))	Merge.kif 4850-4860	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then for all another integer if the other integer is a member of (@ROW), then the integer mod the other integer is equal to 0
(=> (and (equal (LeastCommonMultipleFn @ROW) ?NUMBER) (not (equal ?NUMBER 0))) (not (exists (?LESS) (and (lessThan ?LESS ?NUMBER) (forall (?ELEMENT) (=> (inList ?ELEMENT (ListFn @ROW)) (equal (RemainderFn ?LESS ?ELEMENT) 0)))))))	Merge.kif 4862-4876	If the least common multiple of @ROW is equal to an integer and the integer is not equal to 0, then there doesn't exist another integer such that the other integer is less than the integer and for all a third integer if the third integer is a member of (@ROW), then the other integer mod the third integer is equal to 0
(=> (and (instance ?LEAP LeapYear) (instance ?LEAP (YearFn ?NUMBER))) (or (and (equal (RemainderFn ?NUMBER 4) 0) (not (equal (RemainderFn ?NUMBER 100) 0))) (equal (RemainderFn ?NUMBER 400) 0)))	Merge.kif 8900-8908	If an entity is an instance of leap year and the entity is an instance of the year an integer, then the integer mod 4 is equal to 0 and the integer mod 100 is not equal to 0 or the integer mod 400 is equal to 0
(=> (and (not (equal ?NUMBER2 0)) (equal (AdditionFn (MultiplicationFn (FloorFn (DivisionFn ?NUMBER1 ?NUMBER2)) ?NUMBER2) ?NUMBER) ?NUMBER1)) (equal (RemainderFn ?NUMBER1 ?NUMBER2) ?NUMBER))	Merge.kif 5021-5032	If an integer is not equal to 0 and (the largest integer less than or equal to another integer and the integer and the integer and a third integer) is equal to the other integer, then the other integer mod the integer is equal to the third integer
(=> (instance ?NUMBER EvenInteger) (equal (RemainderFn ?NUMBER 2) 0))	Merge.kif 5044-5047	If an integer is an instance of even integer, then the integer mod 2 is equal to 0
(=> (instance ?NUMBER OddInteger) (equal (RemainderFn ?NUMBER 2) 1))	Merge.kif 5049-5052	If an integer is an instance of odd integer, then the integer mod 2 is equal to 1
(=> (instance ?PRIME PrimeNumber) (forall (?NUMBER) (=> (and (equal (RemainderFn ?PRIME ?NUMBER) 0) (not (equal ?NUMBER 0))) (or (equal ?NUMBER 1) (equal ?NUMBER ?PRIME)))))	Merge.kif 5054-5065	If an integer is an instance of prime number, then for all another integer if the integer mod the other integer is equal to 0 and the other integer is not equal to 0, then the other integer is equal to 1 or the other integer is equal to the integer

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

Show without tree

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