Žinynas
Žinių pagrindai
Tyrinėkite sąvokas, dėsnius, lygtis ir metodus, jų taikymą ir šaltinius. Pasirinkite pažinimo sritį arba raskite konkretų žinyno įrašą.
Daugiau filtrų
Logika ir verifikavimas
Rodoma įrašų: 1–9 iš 9
QMA suteikia polinominio laiko kvantiniam tikrintojui liudytoją, sudarytą iš polinominio skaičiaus kubitų: „taip“ atvejais priimamas bent vienas liudytojas, o „ne“ atvejais atmetami visi liudytojai, esant aprėžtam pilnumo ir patikimumo skirtumui.
Matematinis teiginysInformacijaInteraktyvūs įrodymai ir kvantoriais apibrėžtas pagrįstumasInteraktyvus įrodymas leidžia polinominiu laiku veikiančiam atsitiktinumą naudojančiam tikrintojui keistis pranešimais su skaičiavimo ištekliais neapribotu įrodinėtoju.
ApibrėžimasInformacijaIP=PSPACE ir polinomų suderinamumo patikrosLygybė IP=PSPACE taikoma polinominiu laiku atliekamam atsitiktiniam tikrinimui, kai sąveikų skaičius polinominis, o įrodinėtojas neapribotas.
Matematinis teiginysInformacijaNulinis žinojimas kaip simuliavimo savybėNulinis žinojimas reikalauja efektyvaus simuliatoriaus, kuris be liudijimo (witness) atkuria tikrintojui leidžiamą matyti informaciją pagal nurodytą tikslų, statistinį arba skaičiavimu grindžiamą neatskiriamumą.
ApibrėžimasInformacijaTikimybiškai tikrinami įrodymai ir užklausos į atskiras jų vietasPCP teorema išreiškia NP=PCP(O(log n),O(1)): polinominiu laiku veikiantis tikrintojas naudoja logaritminį atsitiktinių bitų skaičių ir užklausia pastovų vietų skaičių polinominio ilgio įrodyme; pilnumas lygus vienetui, o klaidingo priėmimo tikimybė apribota, pavyzdžiui, viena antrąja.
Matematinis teiginysInformacijaKompiuteriu tikrinami įrodymai, specifikacijos ir patikimi komponentaiĮrodymų asistentas patikrina, ar termas įrodo formalų teiginį pagal nurodytas aksiomas ir branduolio taisykles.
MetodasInformacijaPatikrintas kompiliavimas ir jo pasitikėjimo ribaPagrindinė CompCert semantikos išsaugojimo teorema susieja priimtą C abstrakčiąją sintaksę su sugeneruota asemblerio abstrakčiąja sintakse: esant teoremos prielaidoms, sugeneruota elgsena patikslina leidžiamą pradinės programos elgseną.
MetodasInformacijaCompCert 3.18: datuotas formalios patikros pokytisOficiali CompCert 3.18 laida, išleista 2026 m. rugpjūtį, pakeičia formalų alignment/free tvarkymą ir prideda Rocq 9.2 palaikymą.
MetodasInformacijaDuomenų tipai ir tikrinimasTipai aprašo reikšmes ir leidžiamas operacijas; patikros atliekamos skirtingais etapais.
Apibrėžimas