Naszym celem jest teraz zdecydować, czy KB|= α za jakieś zdanie α. Na przykład, ¬P1,2 wiąże się z naszym KB ? Nasz pierwszy algorytm wnioskowania to podejście polegające na sprawdzaniu modelu, które jest bezpośrednią implementacją definicji wnioskowania: należy wyliczyć modele i sprawdzić, czy α jest prawdziwy w każdym modelu, w którym KB jest prawdziwy. Modele to przypisania prawdy lub fałszu do każdego symbolu zdania. Wracając do naszego przykładu wumpus-world, odpowiednie symbole zdań to B1,1,B2,1 ,P1,1 ,P1,2 ,P2,2, i P3,1 . Z siedmioma symbolami, istnieje 27 = 128 możliwych modeli; w trzech z nich KB jest prawdą. W tych trzech modelach ¬P1,2 to prawda, stąd nie ma wgłębienia w [1,2]. Z drugiej strony P2,2jest prawdziwe w dwóch z trzech modeli, a fałszywe w jednym, więc nie możemy jeszcze stwierdzić, czy w [2,2] jest dół.
Ogólny algorytm decydowania o wynikaniu w logice zdań pokazano na poniżej. Jak algorytm BACKTRACKING-SEARCH, TT-ENTAILS? wykonuje rekurencyjne wyliczenie skończonej przestrzeni przypisań do symboli. Algorytm jest poprawny, ponieważ bezpośrednio implementuje definicję implikacji, i kompletny, ponieważ działa dla każdego KB i α zawsze się kończy – jest tylko skończenie wiele modeli do zbadania.
Oczywiście „skończenie wiele” nie zawsze oznacza „niewiele”. Jeśli KB i α zawierają symbole we wszystkich, to istnieją 2n modele. Zatem złożoność czasowa algorytmu wynosi O(2n). (Złożoność przestrzenna to tylko O(n) ponieważ wyliczenie jest na pierwszym miejscu.) W dalszej części tego pokażemy algorytmy, które w wielu przypadkach są znacznie wydajniejsze. Niestety, wywodzenie zdań jest co-NP-zupełnych (tj. prawdopodobnie nie łatwiejsze niż NP-zupełne), więc każdy znany algorytm wnioskowania dla logiki zdań ma złożoność najgorszego przypadku, która jest wykładnicza pod względem wielkości danych wejściowych.