powrót do strony głównej >>

Sprawdzanie wartości logicznych wyrażeń zdaniowych

Copyright © 2004   Robert Nowotniak
Instytut Informatyki, Politechnika Łódzka




Wpisz wyrażenie, by zobaczyć matrycę logiczną zdania (dostępne operatory):



Poniższa tabela umożliwia sprawdzenie podstawowych tautologii:

~~p <=> pprawo podwójnego przeczenia
p v (~p)prawo wyłączonego środka
(p v p) <=> pprawo idempotentności alternatywy
(p ^ p) <=> pprawo idempotentności koniunkcji
(p v F) <=> pprawo identyczności dla alternatywy
(p ^ T) <=> pprawo identyczności dla koniunkcji
(p ^ q) <=> (q ^ p)prawo przemienności koniunkcji
[(p^q)^r] <=> [p^(q^r)]prawo łączności koniunkcji
(p v q) <=> (q v p)prawo przemienności alternatywy
[(p v q) v r] <=> [p v (q v r)]prawo łączności alternatywy
(p<=>q) <=> (q<=>p)prawo przemienności równoważności
[p^(q v r)] <=> [(p^q)v(p^r)]prawo rozdzielności koniunkcji względem alternatywy
[p v (q^r)] <=> [(p v q)^(p v r)]prawo rozdzielności alternatywy względem koniunkcji
[(p=>q)^(q=>r)] => (p=>r)prawo przechodniości implikacji
[(p<=>q)^(q<=>r)] => (p=>r)prawo przechodniości równoważności
~(p^q) <=> (~p v ~q)prawo De Morgana zaprzeczenia koniunkcji
~(p v q) <=> (~p ^ ~q)prawo De Morgana zaprzeczenia alternatywy
~(p=>q) <=> (p^~q)prawo zaprzeczenia implikacji
(p=>q) <=> (~q=>~p)prawo kontrapozycji
[(p=>q)^(q=>p)] => (p<=>q)związek między implikacją a równoważnością
[(p^q)=>r] <=> [p=>(q=>r)]prawo ekstraportacji
(~p=>F) => pprawo Claviusa
(p=>q) <=> [(p^~q)=>F]prawo reductio ad absurdum
[p^(p=>q)] => qreguła odrywania
[(p=>q)^(r=>s)] => [(p v r)=>(q v s)]pierwsze prawo dylematu konstrukcyjnego
[(p=>q)^(r=>s)] => [(p^r)=>(q^s)]drugie prawo dylematu konstrukcyjnego
p => (p v q)prawo wprowadzania alternatywy
(p^q) => pprawo opuszczania koniunkcji
[(p=>q)^~q]=>~pprawo modus tollendo tollens
[(p v q)^~p] => qprawo modus ponendo tollens
(a+b) <=> (a v b)^~(a^b)Określenie alternatywy wyłączającej
 
Kreska Scheffer'a (nand)
(a|b) <=> ~(a^b)Określenie kreski Scheffer'a
(~a) <=> (a|a)Wyrażenie negacji kreską Scheffer'a
(a ^ b) <=> (a|b)|(a|b)Wyrażenie koniunkcji kreski Scheffer'a
(a v b) <=> (a|a)|(b|b)Wyrażenie alternatywy kreską Scheffer'a
(a=>b) <=> [a|(b|b)]Wyrażenie implikacji kreską Scheffer'a
 
Sklejanie i łączenie formuł boolowskich
(x^y) v (x ^ ~y) <=> x
(~x v y) ^ (x v ~y) <=> (x^y) v (~x ^ ~y)
(a v x)^(a v ~x) <=> a


Poniższa tabelka pokazuje rozpoznawane przez program operatory i ich kolejność. W szczególności, zauważmy, że alternatywa wiąże tak samo silnie jak koniunkcja, więc należy używać nawiasów.

Dozwolone funktory zdaniotwórcze:
{}    []    () grouping
~ negation
v    ^    +    | alternative, conjunction, xor, nand
=> implication
<=> biconditional



Możesz pobrać kod źródłowy programu w Adzie95: tautolog.adb
[Rozmiar: 27.30 KB     Cksum: bf2d0eba1d45cda030fbbc1250a56928 ]



Copyright © Robert Nowotniak
26 stycznia 2004