| ~~p <=> p | prawo podwójnego przeczenia |
| p v (~p) | prawo wyłączonego środka |
| (p v p) <=> p | prawo idempotentności alternatywy |
| (p ^ p) <=> p | prawo idempotentności koniunkcji |
| (p v F) <=> p | prawo identyczności dla alternatywy |
| (p ^ T) <=> p | prawo 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) => p | prawo Claviusa |
| (p=>q) <=> [(p^~q)=>F] | prawo reductio ad absurdum |
| [p^(p=>q)] => q | reguł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) => p | prawo opuszczania koniunkcji |
| [(p=>q)^~q]=>~p | prawo modus tollendo tollens |
| [(p v q)^~p] => q | prawo 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: | |
| {} [] () | grupowanie |
| ~ | negacja |
| v ^ + | | alternatywa, koniunkcja, xor, nand |
| => | implikacja |
| <=> | równoważność |
Copyright ©
Robert Nowotniak
26 stycznia 2004