De Bruijn - kriteeri on hollantilaisen tutkijan Nicholas de Bruijnin laatima empiirinen kriteeri automaattisen lauseentodistusohjelmiston luotettavuudelle .
Lauseentodistaja täyttää de Bruijn-kriteerin, jos tuloskieli, jolla se luo todistetekstin, on pieni ja kompakti, vaikka järjestelmä käyttää monimutkaisia ja resursseja vaativia toimenpiteitä löytääkseen itse todisteen [1] .
Kriteeri muotoiltiin kompaktiksi lauseeksi automaattisen lauseentodistustyökalun menettelyjen toteutuksen näkyvyyden vaatimuksesta . Se tarkoittaa, että vaikka emme pystyisikään täysin varmistamaan todisteiden hakumenettelyjen oikeellisuutta, meidän pitäisi pystyä tarkastamaan itse todisteen automaattisesti luodun esityksen järjestelmän käsittelyn oikeellisuus ja erityisesti toteutuksen oikeellisuus. ytimestä, joka toteuttaa tämän käsittelyn [1] . Tällainen tarkistus voidaan toteuttaa esimerkiksi siten, että skeptinen käyttäjä voi itsenäisesti kirjoittaa pienen ohjelman tarkistaakseen yhden tai useamman automaattisen lauseentodistustyökalun tuottaman todistuksen, toteuttaen saman todistuksen esityskielen kehittämisen kuin tämä työkalu. käyttää [2] . Ymmärretään, että jos molemmat vaihtoehdot tietyn todisteen tarkistamiseksi - alkuperäinen ja skeptinen käyttäjä - toimivat samalla tavalla, tämä lisää merkittävästi luottamusta alkuperäisen automaattisen todistusjärjestelmän toteutuksen laatuun.