Ծառայության պայմաններ
1. Ի՞նչ է ծառայությունը անում
Դուք ներկայացնում եք պահանջ և ստանդարտ։ Մենք այն անցկացնում ենք ձեր ընտրած արհեստական բանականության մոդելների խումբը, ինչպես նաև դատավորի մոդել, որը որոշում է ընդունման կանոնները, և մենք փորձում ենք ֆորմալացնել արդյունքը Lean 4-ի և Mathlib-ի միջև։ Էքսպորտային տվյալները տեքստն են, որոշումների հավաքածուն, դատավճիռը, և որտեղ ֆորմալացման փորձ է արվել, Lean արդյունքը։
2. Ի՞նչ է ելքը և ի՞նչ ոչ
Էլեկտրոնային նամակները թողարկվում են ինտերնետում, բայց ոչ ինտերնետային ծառայություններում։ Այն չի հանդիսանում իրավական, բժշկական, ֆինանսական, ինժեներական կամ որևէ այլ տեսակի մասնագիտական խորհուրդ, և այս ծառայությունը օգտագործելով ոչ մի մասնագիտական հարաբերություն չի ստեղծվում։
Խաղի արդյունքը որոշելու համար դատավորը պետք է հաշվի առնի խաղի ընթացքում ստացված ապացույցները։ Սա ճշգրտության երաշխիք չէ։ ԱԻ մոդելները սխալներ են գործում, սխալ են կարդում աղբյուրները և կարող են կառուցել մեջբերումներ՝ չնայած ոչ մի հրահանգի։ Դուք պետք է ինքնուրույն ստուգեք այն ամենը, ինչին ցանկանում եք վստահել։, հատկապես հրապարակելուց, ներկայացնելուց կամ գործողություն կատարելուց առաջ։ Սա գործիք է ճնշման փորձարկման համար, որը չի փոխարինում որակյալ մարդկային վերլուծությունը։
Հաջող Lean ֆորմալացումը նշանակում է, որ Lean kernel- ը ընդունել է փաստարկված հայտարարության փաստը, որը ֆորմալացվել է, օգտագործելով Mathlib տարբերակը, որը օգտագործվում էր այդ ժամանակ։ Դա չի նշանակում, որ այդ հայտարարությունը հավաստի թարգմանություն է ձեր խնդրածի, և ֆորմալ հայտարարություն ընտրելը, որը չի ասում այն, ինչ դուք ուզում եք ասել, ամենատարածված ձևն է, որով ֆորմալ արդյունքը ձեզ կսխալեցնի։ Կարդացե՛ք ֆորմալ հայտարարությունը, ոչ միայն դատավճիռը։
Ձեր պարունակությունը
Դուք պահպանում եք ձեր ներկայացրած պահանջների և ձեզ համար ստեղծված արտադրանքի սեփականությունը։ Դուք մեզ տալիս եք միայն ծառայությունը գործարկելու համար անհրաժեշտ թույլտվությունը՝ ձեր ներկայացրածը վերամշակելու, այն փոխանցելու ձեր ընտրած մոդելի մատակարարներին և պահպանելու արդյունքում ստացված համապատասխանությունը, որպեսզի կարողանաք վերադառնալ այն։
Համապատասխանությունները լռելյայն մասնավոր են։ Եթե դուք նշեք համապատասխանությունը հանրային, այն տեսանելի կդառնա հղում ունեցող ցանկացած անձի համար և կարող է հայտնվել մեր հանրային պատկերասրահում։ Չհրապարակեք համապատասխանություն, որը պարունակում է գաղտնի տեղեկատվություն։
Չներկայացնել այլ մարդկանց մասին անձնական տվյալներ, գաղտնի նյութեր, որոնք դուք իրավունք չունեք կիսել, կամ անօրինական բովանդակություն։
4. Կրեդիտներ և հաշվարկներ
Կրեդիտը նախօրոք վճարված է և օգտագործվում է խաղի ընթացքում։ Յուրաքանչյուր խաղ ունի ծախսման սահմանափակում, որը դուք եք սահմանում։ Այն հասնելու դեպքում խաղը դադարեցվում է, այլ ոչ թե շարունակվում։ Կրեդիտը չի փոխանցվում և, բացի այն դեպքերից, երբ օրենքը պահանջում է, չի փոխհատուցում օգտագործման դեպքում։ Անօգտագործված կրեդիտը պահանջի դեպքում վերադարձվում է։
Եթե դուք միացնում եք ձեր սեփական եզրակացության կոդը, դուք ուղղակիորեն վճարում եք ձեր ծառայության մատակարարին և մենք չենք հաշվարկում յուրաքանչյուր տոկենի համար վճարը։ Առանց վճարի ծառայության ցուցադրման դեպքում կիրառվում է ինֆրակառուցվածքի վճար՝ պրոցեսի, գործիքների և պահպանման ընթացքը ծածկելու համար։
Մենք կարող ենք փոխել գները նախապես տեղեկացնելով։ Փոփոխությունները երբեք չեն վերաբերում արդեն գնված վարկերին։
Օգտագործման թույլտվություն
Չօգտագործեք ծառայությունը այլ մարդկանց վնասելու նպատակով, մեր հրահանգները կամ համակարգի հրահանգները դուրս բերելու համար, ծախսերի կամ արժեքի սահմանափակումները խախտելու համար, կամ առանց գրավոր համաձայնության մուտք գործելու իրավունքը վերավաճառելու համար։ Կոդը կատարելու գործիքը նախատեսված է պահանջները ստուգելու համար, չօգտագործեք այն որևէ համակարգի վրա հարձակվելու համար։
Վերջնական
Մենք կախված ենք երրորդ կողմի մոդելի մատակարարներից։ Մատակարարները կարող են ջարդվել, փոխել մոդելները և դրանք հնացած համարել։ Որևէ պատճառով դադարեցված համապատասխանությունը դադարեցվում է և վերսկսվում։ Մենք չենք վճարում այն աշխատանքի համար, որը տեղի չի ունեցել։ Մենք չենք երաշխավորում անխափան հասանելիությունը, և մոդելը, որը դուք օգտագործել եք նախորդ անգամ, կարող է դառնալ հասանելի։
Պատասխանատվություն
Օրենքի թույլատրելի առավելագույն չափով, ծառայությունը մատուցվում է այնպիսին, ինչպիսին այն է, առանց որևէ տեսակի երաշխիքի։ Մեր ընդհանուր պատասխանատվությունը ցանկացած պահանջի համար սահմանափակվում է այն գումարով, որը դուք վճարել եք մեզ պահանջի առաջացմանից երեք ամիս առաջ։ Մենք չենք պատասխանատու անուղղակի կամ հետևանքային վնասների համար, ներառյալ մոդելի արտահոսքի վրա հիմնված ցանկացած վնաս։
Դադար
Դուք կարող եք ցանկացած պահի փակել ձեր հաշիվը, և մենք կվերադարձնենք չօգտագործված վարկային գումարը։ Մենք կարող ենք արգելափակել հաշիվները, որոնք խախտում են այս պայմանները կամ ծառայությունը վտանգի են ենթարկում։
9. Փոփոխություններ, լեզուն և կապը
Մենք կարող ենք այս պայմանները նորացնել, և նյութական փոփոխությունները կհայտարարվեն կայքում։
Այս էջի թարգմանությունները մատուցվում են հեշտության համար և մեքենային են վերագրվում։ Եթե թարգմանությունը և անգլերեն տարբերակը տարբերվում են, անգլերեն տարբերակը գերակշռում է։
Հարցեր: Համագործակցել մեզ հետ.