Systém automatického dokazovania pomocou rezolúcie

Priorita operátorov:

1. Negácia (¬)
2. Negovaná Konjunkcia (↑)
3. Negovaná Disjunkcia (↓)
4. Negovaná Implikácia (⇏)
5. Exkluzívna Disjunkcia (⊕)
6. Konjunkcia (∧)
7. Disjunkcia (∨)
8. Implikácia (⇒)
9. Ekvivalencia (⇔)

Vstup a výstup

V ľavej časti je možné nastaviť veľkosť písma vo vstupnom aj výstupnom poli.
V pravej časti je možné si zvoliť vzhľad stránky.

Pre vyhodnotenie formuly zadajte formulu do vstupného poľa pomocou kláves pod poľom, alebo jednoducho doňho skopírujte formulu z LaTeXu. Taktiež je možné formuly zadať ručne, všetky možné akceptované tvary operátorov sú vypísané v časti "Syntax". Vstupné pole obsahuje kontrolu syntaxe.

Po stlačení tlačidla "POTVRĎ" sa na stránke objaví okno výstupu, do ktorého ľavej časti sa vypíšu nasledovné údaje:

• Zadaná formula: formula načítaná zo vstupného poľa.
• Zjednodušená formula: ak formula obsahuje prebytočné zátvorky alebo viacnásobné negácie, budú z nej odstránené.
• Negácia formuly: Postup, ako negovať danú formulu. Operátory, ktoré sú v danom kroku negované sú zvýraznené červenou farbou.
• Negovaná formula: Výsledok negácie formuly

Následne bude formula prevedená do Konjunktívnej Normálnej Formy (KNF). To sa deje pomocou nasledujúcich krokov:

1. Odstránenie implikácie a ekvivalencie: zvýraznené implikácie/ekvivalencie sú v nasledujúcom kroku prepísané následovne:
φ ⇔ ψ ≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ) ≡ (¬φ ∨ ψ) ∧ (¬ψ ∨ φ)
φ ⇒ ψ ≡ ¬φ ∨ ψ


2. Vloženie negácie do zátvorky a odstránenie operátorov ↑, ↓, ⇏, ⊕:
¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
φ ↑ ψ ≡ ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ
φ ↓ ψ ≡ ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ
φ ⇏ ψ ≡ ¬(φ ⇒ ψ) ≡ ¬(¬φ ∨ ψ) ≡ φ ∧ ¬ψ
φ ⊕ ψ ≡ ¬(φ ⇔ ψ) ≡ ¬((¬φ ∨ ψ) ∧ (¬ψ ∨ φ)) ≡ φ ∧ ¬ψ ∨ ψ ∧ ¬φ


3. Vloženie disjunkcií do vnútra zátvoriek:
φ ∨ (ψ ∧ θ) ≡ (φ ∨ ψ) ∧ (φ ∨ θ)
(ψ ∧ θ) ∨ φ ≡ (ψ ∨ φ) ∧ (θ ∨ φ)
(φ ∧ ψ) ∨ (θ ∧ ω) ≡ (φ ∨ θ) ∧ (φ ∨ ω) ∧ (ψ ∨ θ) ∧ (ψ ∨ ω)


4. Zjednodušenie odstránením klauzúl s komplementárnymi literálmi, duplicitných klauzúl a duplicitných literálov:
¬φ ∨ φ ≡ ⊤
(φ ∨ ψ) ∧ (ψ ∨ φ) ≡ φ ∨ ψ
φ ∨ ψ ∨ φ ≡ φ ∨ ψ

Ak niektorý z týchto krokov nespôsobil žiadnu zmenu vo formule, nebude vo výstupnom okne vypísaný.

• Negovaná KNF: Výsledok prevodu do KNF
• Množinová notácia: prevod KNF do množinovej notácie
• Na konci je vypísaný výsledok rezolúcie, teda či daná formula je alebo nie je tautológia.

Pod vstupným poľom je možné nastaviť stratégiu rezolúcie, a spôsob výpisu stromu.

Stratégie rezolúcie:

• Úplná - program sa pokúsi spojiť každú klauzulu s každou aby dosiahol výsledok rezolúcie. Prioritizuje však najprv jednotkové klauzuly.
• Jednotková - program pri každej rezolúcií musí použiť aspoň jednu jednotkovú klauzulu.
• Lineárna - program vždy využije v ďalšom kroku rezolventu predchádzajúceho kroku.

Redukovaný strom - Namiesto toho, aby boli v strome zobrazené všetky klauzuly a rezolventy, budú v ňom zobrazené len tie, ktoré viedli k výsledku.
V pravej časti výstupného okna je možnosť prepnúť medzi dvoma reprezentáciami rezolúcie, a to:

• Rezolučná tabuľka: V tejto tabuľke sú uvedené všetky klauzuly a rezolventy v množinovej notácií v druhom stĺpci. Tabuľka uvádza postup rezolúcie, ktorý bol použitý na zistenie, či zadaná formula je tautológia. Klauzuly a rezolventy sú očíslované v prvom stĺpci tabuľky. V tretom stĺpci tabuľky je uvedené, ktoré klauzuly boli použité na vytvorenie danej rezolventy pomocou rezolúcie.
• Rezolučný strom: Podľa zvoleného spôsobu rezolúcie a výpisu stromu bude tento strom obsahovať kroky vedúce k výsledku rezolúcie.

Všetky časti výstupu, teda textový výstup, tabuľku a strom je možné kopírovať pomocou tlačidiel umiestnenými pod oknom výstupu do formy LaTeX-ového kódu. Tabuľka je prevedená do formy tabular a strom je prevedený do obrázku formy tikz.