Ekvivalence dvou formulí výrokove logiky

[pan]

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

[Reklama]

[tadeas]

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

[Radek Miček]

Na System on TPTP 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í.