Systém automatického dokazovania pomocou rezolúcie
Rezolúcia
Syntax
Manuál
Pravdivostné tabuľky
16px
18px
24px
32px
48px
Veľkosť písma:
Morning
Noon
Sunset
Midnight
Matrix
Výber motívu:
Výstup
Rezolučný strom
Rezolučná tabuľka
Kopírovať Výstup
Všetko
Úprava formuly
Kroky negácie formuly
Negácia formuly
Kroky prevodu na KNF
Formula v KNF
Množinová notácia
Kopírovať Strom
Kopírovať Tabuľku
Skopírované
---
Jednoduchý vstup
Symbolický vstup
LaTeX vstup
ASCII vstup
DIMACS vstup
Príklady:
Toto pole je povinné
POTVRĎ
Stratégia rezolúcie:
Úplna
Jednotková
Lineárna
Redukovaný strom
Plne zátvorkovaná formula
