Siatki próbne są interesujące zasadniczo z trzech powodów:
1) TOŻSAMOŚĆ DOWODÓW. Stanowią odpowiedź na problem „kiedy dwa dowody są takie same”? W rachunku różniczkowym możesz mieć wiele różnych dowodów tej samej twierdzenia, które różnią się tylko tym, że rachunek różny wymusza porządek wśród reguł dedukcyjnych, nawet jeśli nie jest to konieczne. Oczywiście można dodać relację równoważności do kolejnych dowodów rachunku różniczkowego, ale potem trzeba wykazać, że eliminacja cięć zachowuje się poprawnie w klasach równoważności, a także konieczne jest przejście do przepisywania modulo, które jest o wiele bardziej techniczne niż zwykłe przepisywanie. Sieci sprawdzające rozwiązują problem radzenia sobie z klasami równoważności, zapewniając składnię, w której każda klasa równoważności jest zwinięta na jednym obiekcie. Ta sytuacja jest i tak nieco idealistyczna, ponieważ z wielu powodów sieci dowodowe są często rozszerzane o pewną formę równoważności.
2) BRAK KOMUTATYWNYCH KROKÓW ELIMINACJI. Eliminacja cięć w siatkach próbnych przybiera zupełnie inny smak niż w sekwencyjnych rachunkach, ponieważ znikają etapy przemiennej eliminacji cięć. Powodem jest to, że w sieciach dowodowych reguły odliczeń są powiązane jedynie ich relacją przyczynową. Przypadki przemienne generowane są przez fakt, że jedną regułę można ukryć za pomocą innej przyczynowo niezwiązanej reguły. Nie może się to zdarzyć w sieciach dowodowych, w których reguły przyczynowo niepowiązane są daleko od siebie. Ponieważ większość przypadków eliminacji cięć ma charakter przemienny, uzyskuje się uderzające uproszczenie eliminacji cięć. Jest to szczególnie przydatne do badania rachunku lambda z wyraźnymi podstawieniami (ponieważ wykładnicze = wyraźne podstawienia). Ponownie sytuacja ta jest idealizowana, ponieważ niektóre prezentacje sieci próbnych wymagają kroków przemiennych. Jednak,
3) KRYTERIA POPRAWNOŚCI. Siatki próbne można zdefiniować przez tłumaczenie kolejnych dowodów rachunku różniczkowego, ale zwykle system siatek dowodowych nie jest jako taki akceptowany, chyba że jest wyposażony w kryterium poprawności, tj. Zbiór zasad teoretyczno-graficznych charakteryzujących zbiór wykresów uzyskany przez przetłumaczenie kolejny rachunek różniczkowy. Powodem wymagania kryterium poprawności jest to, że wolny język graficzny generowany przez zestaw konstruktorów sieci proof (zwanych linkami) zawiera „zbyt wiele grafów”, w tym sensie, że niektóre wykresy nie odpowiadają żadnym dowodom. Znaczenie podejścia opartego na kryteriach poprawności jest zwykle całkowicie niezrozumiane. Jest to ważne, ponieważ daje nieindukcyjne definicje tego, co jest dowodem, zapewniając szokująco odmienne spojrzenie na charakter dedukcji. Fakt, że charakterystyka jest nieindukcyjna, jest zwykle krytykowany, podczas gdy jest dokładnie tym, co interesujące. Oczywiście nie jest łatwo poddać się formalizacji, ale znowu taka jest jego siła: siatki dowodowe zapewniają wgląd, który nie jest dostępny w zwykłej indukcyjnej perspektywie na dowodach i warunkach. Fundamentalnym twierdzeniem dla siatek dowodowych jest twierdzenie sekwencjonowania, które mówi, że każdy wykres spełniający kryterium poprawności może być indukcyjnie rozłożony jako sekwencyjny dowód różniczkowy (przełożenie z powrotem na prawidłowy wykres).
Pozwolę sobie stwierdzić, że nie jest precyzyjne stwierdzenie, że siatki dowodowe to klasyczna i liniowa wersja naturalnej dedukcji. Chodzi o to, że rozwiązują (lub próbują rozwiązać) problem tożsamości dowodów i że naturalna dedukcja z powodzeniem rozwiązuje ten sam problem przy minimalnej intuicyjnej logice. Ale siatki dowodowe można wykonać również w przypadku systemów intuicyjnych i systemów nieliniowych. W rzeczywistości działają lepiej dla systemów intuicyjnych niż dla systemów klasycznych.