CanProve .

Überprüfen logischer Aussagen


CanProve

mathematische Standardbibliothek
Funktionsaufruf:
CanProve(proposition)
Parameter:
proposition - eine logische Aussage
Beschreibung:
Mit dieser Funktion lassen sich logische Aussagen überprüfen.
Ein Beispiel für eine logische Aussage ist:
Wenn aus a b folgt und aus b c, dann folgt aus a c.
Yacas unterstützt folgende Operatoren:

Not   Negation
And  UND
Or    ODER
=>    daraus folgt

Das angegebene Beispiel lautet dann:

( (a=>b) And (b=>c) ) => (a=>c)

Mit Hilfe von CanProve kann die Richtigkeit der Aussage überprüft werden:

In> CanProve(( (a=>b) And (b=>c) ) => (a=>c))
Out> True;

Die Funktion versucht die Aussage "p" zu beweisen, indem gezeigt wird, dass Not p falsch ist. Not p wird dazu schrittweise mit Hilfe folgender Regeln vereinfacht:

Not  ( Not x)  -->  x                      eliminate double negation
x=>y           -->  Not x  Or  y           eliminate implication
Not (x And y)  -->  Not x  Or  Not y       De Morgan's law
Not (x  Or  y) -->  Not x  And Not y       De Morgan's law
(x And y) Or z -->  (x Or z) And (y Or z)  Distribution
x Or (y And z) -->  (x Or y) And (x Or z)  Distribution

Durch Anwendung der Regeln wird die logische Aussage in folgende Form gebracht:

(p1  Or  p2  Or  ...)  And  (q1  Or  q2  Or  ...)  And ...

Ist einer der Klammerausdrücke logisch falsch, ist der gesammte Ausdruck falsch.
Beispiele:
In> CanProve(a  Or   Not a)
Out> True;

In> CanProve(True  Or  a)       
Out> True;

In> CanProve(False  Or  a)      
Out> a;

In> CanProve(a  And   Not a)         
Out> False;

In> CanProve(a  Or b Or (a And b))     
Out> a Or b;
siehe auch:
True , False , And , Or , Not .