Quit[]

Elementy logiki, rachunek zdań, kwantyfikatory

Operatory i wyrażenia logiczne

Notacja logiczna w Mathematice jest identyczna jak w C.

Negacja (Not)

Operator "nie" oznaczony jest wykrzyknikiem

!x

Operator negacji w zdaniu

!3==4

Nierówny  (Unequal, !=, ≠)

3!=4

Lub (Or, || ,∨)

Alternatywa: operator lub

x == x || y != y

W postaci tradycyjnej

x==x∨y≠y

x≠x∨x==y

False||!False;

False∨¬False

Koniunkcja (And, &&, ∧)

x==x&&y==y;

x==x∧y==y

(1<2)&&!(4<2);

1<2∧¬4<2

Implikacja (Implies, =>)

Implies[1<4,1<8];

1<4\[Implies]1<8

Boole

Funkcja Boole zamienia wartosć logiczną True na liczbę 1 i wartość logiczna False na liczbe 0

Boole[True]

Boole[False]

Zamiana list na wyrażenia logiczne i odwrotnie

And@@{(x^2)+(y^3)-(z^2)>0,(x^2)+(y^2)+(z^2)>2}
List@@ %

Or@@{x y z>1,(x^2)+(y^2)+(z^2)<20}

Solve i Reduce raz jeszcze

Polecenie Solve domniemuje, że wartości zmiennych spełniają dodatkowe kryteria (np. zmienna, przez którą dzielimy nie przyjmie wartości zero).

Solve[a (x^2)+b x +c==0,x]

Polecenie Reduce jawnie podaje wszystkie możliwości w formie wyrażenia logicznego

Reduce[a (x^2)+b x +c==0,x]

Rezultat Reduce można zamienić na listę wskazań (Rules)

%[[1,2]]
Solve[%,x]

Rachunek zdań (przykłady)

Przykład 1.

A=(a||!b)&&(b||!a)&&(b||a);
A=Simplify[A];
A

A=(a∨¬b)∧(b∨¬a)∧(b∨a);
A=Simplify[A];
A//TraditionalForm

Przykład 2.

A=(a||!b)&&(b||!c)&&(c||!a);
A=Simplify[A];
A

A=(a∨¬b)∧(b∨¬c)∧(c∨¬a);
A=Simplify[A];
A//TraditionalForm

Przykład 3.

A=(a||!b&&c)&&(b||!c&&a)&&(c||!a&&b);
A=Simplify[A];
A

A=(a∨(¬b∧c))∧(b∨(¬c∧a))∧(c∨(¬a∧b));
A=Simplify[A];
A//TraditionalForm

Przykład 4.

A=((a||!b)&&c)&&((b||!c)&&a)&&((c||!a)&&b);
A=Simplify[A];
A

A=((a∨¬b)∧c)∧((b∨¬c)∧a)∧((c∨¬a)∧b);
A=Simplify[A];
A//TraditionalForm

Implies[A,a]//Simplify

A\[Implies]a//Simplify

w jednej linii:

((a∨¬b)∧c)∧((b∨¬c)∧a)∧((c∨¬a)∧b)\[Implies]a   ;
%//Simplify

Kwantyfikatory - "dowodzenie twierdzeń" (*)

Dla każdego (ForAll, Resolve)

Nierównosć trójkata

ForAll[{x,y},(x|y)∈Reals,Abs[x + y]<=Abs[x]+Abs[y]]//Resolve

(Subscript[∀, {x,y},(x|y)∈ Reals])(Abs[x+y]≤Abs[x]+Abs[y])//Resolve

(Subscript[∀, {x,y},(x|y)∈ℝ]) \[LeftBracketingBar]x+y\[RightBracketingBar]≤\[LeftBracketingBar]x\[RightBracketingBar]+\[LeftBracketingBar]y\[RightBracketingBar]//Resolve

Resolve[(Subscript[∀, {x,y},(x|y)∈ Complexes])(Abs[x+y]≤Abs[x]+Abs[y])]

(Subscript[∀, {x,y},(x|y)∈ℂ])\[LeftBracketingBar]x+y\[RightBracketingBar]≤\[LeftBracketingBar]x\[RightBracketingBar]+\[LeftBracketingBar]y\[RightBracketingBar]//Resolve

Inne nierówności

(Subscript[∀, {x,y},(x|y)∈ Reals])(Abs[x]-Abs[y]≤Abs[x-y])//Resolve

(Subscript[∀, {x,y},(x|y)∈ Reals])(Abs[x]-Abs[y]≤Abs[x]+Abs[y])//Resolve

Istnieje (Exists, Resolve)

Granica Cauchy'ego

(Subscript[∀, ϵ,ϵ>0])((Subscript[∃, M,M∈Reals])((Subscript[∀, x,x>M&&λ∈Reals])-ϵ<1+(1/x)-λ<ϵ))//Resolve

(Subscript[∀, ϵ,ϵ>0]) (Subscript[∃, M,M∈Reals])(Subscript[∀, x,x>M &&  λ∈Reals])(-ϵ<1+1/x-λ<ϵ )//Resolve

(Subscript[∀, ϵ,ϵ>0])((Subscript[∃, M,M∈ℝ])((Subscript[∀, x,x>M∧λ∈ℝ])-ϵ<-λ+(1/x)+1<ϵ))//Resolve

Polecenie Resolve jest zaimplementowane w Reduce, 
Reduce jest zaimplementowane w FullSimplify

źródło notatnika

Algebra Komputerowa  (http://mth.drac.oa.uj.edu.pl/public.php?pubcase=lecture)
Wersja programu: Mathematica 7

Andrzej Woszczyna
Wydział Fizyki, Astronomii i Informatyki Stosowanej
Uniwersytet Jagielloński