Jakie kombinacje wejść powodują, że pierwsze wyjście C1 (bit sumy) ma wartość 0, a drugie wyjście C1 (bit przeniesienia) ma wartość 1?
Odpowiedzi są podstawieniami zmiennych i1, i2 oraz i3 w taki sposób, że zdanie wynikowe jest zawarte w bazie wiedzy. ASKVARS da nam trzy takie podstawienia:
Jakie są możliwe zestawy wartości wszystkich zacisków dla obwodu sumatora?
To ostatnie zapytanie zwróci kompletną tabelę wejścia-wyjścia dla urządzenia, która może być użyta do sprawdzenia, czy faktycznie dodaje ono poprawnie swoje dane wejściowe. To jest prosty przykład weryfikacji obwodu. Możemy również wykorzystać definicję obwodu do budowy większych systemów cyfrowych, dla których można przeprowadzić ten sam rodzaj procedury weryfikacji. Wiele dziedzin jest podatnych na ten sam rodzaj ustrukturyzowanego rozwoju bazy wiedzy, w którym bardziej złożone koncepcje są definiowane obok prostszych konceptów.
Debuguj bazę wiedzy
Możemy zaburzać bazę wiedzy na różne sposoby, aby zobaczyć, jakie rodzaje błędnych zachowań się pojawiają. Załóżmy na przykład, że nie przeczytaliśmy sekcji 8.2. 8 i dlatego zapomnij stwierdzić, że 1 ≠ 0. Nagle system nie będzie w stanie udowodnić żadnych wyjść dla obwodu, z wyjątkiem przypadków wejściowych 000 i 110. Możemy wskazać problem, pytając o wyjścia każdej bramki. Na przykład możemy zapytać
co pokazuje, że nie są znane żadne wyjścia dla przypadków wejściowych 10 i 01. Następnie patrzymy na aksjomat dla bramek XOR, jak zastosowano do:
Jeśli wiadomo, że dane wejściowe to, powiedzmy, 1 i 0, to sprowadza się to do
Teraz problem jest oczywisty: system nie jest w stanie tego wywnioskować, Signal(Out(1,X1)) = 1 więc musimy mu powiedzieć, że 1 ≠ 0