Fórum Root.cz

Hlavní témata => Software => Téma založeno: pan 05. 10. 2012, 16:28:51

Název: Ekvivalence dvou formulí výrokove logiky
Přispěvatel: pan 05. 10. 2012, 16:28:51

Nevite o nejakem programu (nejlepe online) ve kterem by se daly srovnat dve logicke formule vyrokove logiky? Zkousel jsem hledat, ale marne.

Název: Re:Ekvivalence dvou formuli vyrokove logiky
Přispěvatel: tadeas 05. 10. 2012, 16:43:23

Možná http://www.wolframalpha.com/

Název: Re:Ekvivalence dvou formuli vyrokove logiky
Přispěvatel: Radek Miček 05. 10. 2012, 17:06:15

Na System on TPTP (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP) jsou k dispozici různé dokazovače, takže stačí zadat formuli ve správné syntaxi a vybrat dokazovač.

Například, když chci dokázat, že (a => a) je ekvivalentní (a <=> a),
tak jako vstup zadám negaci formule ((a => a) <=> (a <=> a)) - tj.:

Kód: [Vybrat]

fof(a, axiom, ~((a => a) <=> (a <=> a))).
Pak zvolím dokazovač Paradox 4.0 a kliknu na RunSelectedSystems.
Výstupem bude

Kód: [Vybrat]

% START OF SYSTEM OUTPUT
Paradox, version 4.0, 2010-06-29.
+++ PROBLEM: /tmp/SystemOnTPTP10044/SOT_kSIzzW.tptp:short
Reading '/tmp/SystemOnTPTP10044/SOT_kSIzzW.tptp:short' ... OK
+++ SOLVING: /tmp/SystemOnTPTP10044/SOT_kSIzzW.tptp:short
+++ RESULT: Unsatisfiable
SZS status Unsatisfiable for /tmp/SystemOnTPTP10044/SOT_kSIzzW.tptp:short

% END OF SYSTEM OUTPUT
% RESULT: SOT_kSIzzW - Paradox---4.0 says Unsatisfiable - CPU = 0.00 WC = 0.01
% OUTPUT: SOT_kSIzzW - Paradox---4.0 says Assurance - CPU = 0.00 WC = 0.01
Paradox tedy říká, že formule je nesplnitelná, tj. její negace je tautologie,
takže ekvivalence platí.