Switch to english
Přepnout do češtiny
Direct proof Důkaz přímým odvozením Proof by contradiction Důkaz sporem Disproof by counterexample Vyvrácení protipříkladem |
|
|
Switch to english
Přepnout do češtiny
Direct proof Důkaz přímým odvozením Proof by contradiction Důkaz sporem Disproof by counterexample Vyvrácení protipříkladem |
|
Záhlaví slouží ke zvolení typu důkazu, vkládání tvrzení na dokazovací prostor a k zadávání příkladů. V dokazovacím prostoru můžete s tvrzeními volně manipulovat a spojovat s dalšími tvrzeními a tvořit tak důkaz.
In the header, you can choose method of proof, add statements to workspace and create the task you want to prove. In the workspace, you can move with statements and join them together to create a proof.
Program rozlišuje 4 typy atomických tvrzení, ze kterých lze důkaz sestavit:
In the application, 4 types of atomic statement can be used in proof:
Obecné tvrzení představuje tvrzení o příslušnosti jazyka do určité jazykové třídy. Tato tvrzení lze znegovat kliknutím na symboly ∈ a ∉.
Language statement represents that language is member of specific language class. This statements can be negated using ∈ and ∉ symbols.
Toto tvrzení znázorňuje uzávěrovou vlastnost jazykové třídy na určitou operaci.
This statement represents closure property of specific language class under specific operation.
Konkrétní tvrzení představuje tvrzení, že nějaký jazyk je roven konkrétnímu jazyku z databáze.
Concrete statement represents that some language is equal to concrete language from database.
Toto tvrzení slouží k odvození sporu z nějakých dvou obecných tvrzení.
This statement is used for deducing contradiction from two language statements.
Pomocí barev se rozlišuje mezi 3 stavy každého tvrzení:
Colors determine 3 states of each statement:
Bílá (neznámé): o tvrzení není známo, zda je pravdivé či nepravdivé.
White (unknown)): it is not known if the statement is true or false.
Zelená (správně): tvrzení je předpokládáno ze zadání nebo bylo korektně odvozeno.
Green (correct): statement can be assumed or it was correctly deduced before.
Červená (nesprávně): tvrzení není nebo nemůže být korektně odvozeno.
Red (wrong): statement cannot be deduced.
Pokud tvrzení obsahuje název jazyka, lze jej po kliknutí upravit v editoru jazyků.
After click, language name in statement can be edited in the editor of languages.
Do textového pole se vpisují názvy atomických jazyků. Type atomic names in the input field.
Pomocí tlačítek se provádí přidání a odebrání operace. Buttons for adding and deleting operations.
Zadávané tvrzení je uvozeno všeobecným kvantifikátorem, což znamená, že pravdivé tvrzení musí platit pro libovolné jazyky.
Task is prefixed with universal quantifier. That means that true statement must be true for all languages.
Symbol implikace slouží k úpravě tvrzení (A ⇒ B) na ekvivalentní (¬B; ⇒ ¬A;) a naopak.
Implication symbol is used for changing statement (A ⇒ B) to equivallent (¬B; ⇒ ¬A;).
Pomocí tlačítek lze přidávat a odebírat tvrzení ze stran implikace. Buttons for adding and deleting statements in task.
Tlačítkem v levém horním rohu se tvrzení vloží do dokazovacího prostoru. This button adds statement to the workspace.
Symbol logické spojky (konjuknce, disjunkce) slouží ke změně všech logických spojek na dané straně implikace.
Symbol of logical connective (conjunction, disjunction) changes all logical connectives on the side of implication.
Pomocí tohoto tlačítka lze s tvrzeními pohybovat v dokazovacím prostoru. On the workspace, you can move with the statement using this button.
Tato tlačítka slouží k vytvoření kopie tvrzení nebo naopak k jeho odstranění. Button for creating copy and deleting of the statement.
Důkaz se sestavuje v dokazovacím prostoru tak, že se jednotlivá atomická tvrzení spojují vazbami.
Proof is created in the workspace using connecting atomic statements with links.
Výběr spojovaných tvrzení se provádí pomocí tlačítek nad a pod tvrzením. Statements that will be joined are selected with buttons above and under the statements.
K vytvoření nebo zrušení vazby mezi tvrzeními musí být vybrán právě jeden horní a právě jeden spodní spojovač.
To create or delete a link, it is necessary to select exactly one top and one bottom joining button.
Vybraný spojovač je zvýrazněn modrou barvou. Selected joining button is highlighted with blue color.
Důkaz čteme shora dolů, vazba tedy jednoznačně určuje dedukční krok. Tvrzení s využitým spodním spojovačem je proto předpokladem a tvrzení s využitým horním spojovačem je závěrem dedukčního kroku.
We read proof from top to bottom, so a link represents deduction step. Therefore, statement with used bottom joining button represents the premise and statement with used bottom joining button represents conclusion of deduction step.
K informování o průběhu a správnosti důkazu slouží textový popis v záhlaví.
Text in the header informs you about progress in proving.
Předpokládejme platnost předpokladů zadané implikace (tvrzení jsou obarvena zeleně). Abychom dokázali platnost celé implikace, musíme buď ukázat, že předpokládaná tvrzení jsou ve sporu a předpoklad implikace tudíž nemůže platit. Nebo musíme z předpokládaných tvrzení odvodit závěr implikace.
Assume the premise of implication is true. To prove that whole implication is true, we have to show that premises are in contradiction or have to deduce conclusion of implication using assumed statements.
Důkaz sporem spočívá v předpokládání platnosti předpokladů implikace a neplatnosti závěru implikace. Pokud z tohoto odvodíme spor, musely být v rozporu už samotné předpoklady (a implikace platí) nebo je spor způsoben mylným předpokladem neplatnosti závěru. V druhém případě nutně musel být původní závěr pravdivý a tedy pravdivá celá implikace.
When proving by contradiction, we assume that the premise of implication is true and the conclusion is false. If we deduce contradiction from assumed statements, conclusion of implication has to be true and therefore whole implication is true.
Pokud vyvracíme obecné tvrzení, vlastně dokazujeme negaci tohoto tvrzení, které je kvantifikováno existenčím kvantifikátorem. Proto nám stačí ukázat, že původní tvrzení pro nějaký konkrétní protipříklad neplatí. Nic tedy nepředpokládáme, pouze se snažíme z konkrétních tvrzení odvodit platnost předpokladů a neplatnost závěru implikace.
Disproving of universal statement is equivallent to proving negation of the statement quantified with existential quantifier. So, to disprove the statement we have to show that statement is false for some counterexample. We don't assume anything, from concrete statements we only try to deduce that premise of the implication is true and the conclusion is false.
Při dokazování lze využít znalosti Chomského hierarchie gramatik a příslušných jazykových tříd. Na následujícím obrázku je tato hierarchie znázorněna, ze kterého je patrná vlastní inkluze mezi třídami. Například, že všechny konečné jazyky jsou regulární, ale ne všechny regulární jazyky jsou konečné.
In proof, you can use facts concerning Chomsky hierarchy of grammars and language classes. In the picture of Chomsky hierarchy, you can see that language classes are in inclusion. For example, every finite language is regular, but not every regular languge is finite.
Jazyková třída je uzavřena na operaci, pokud jazyk vzniklý aplikací dané operace nad libovolnými jazyky z této třídy stále náleží do této třídy. Následující tabulka znázorňuje známé uzávěrové vlastnosti.
Language class is closed under a operation if language created by application of the operation on every language from the language class is still member of the language class. Table shows known closure properties.
Protipříklady jsou konkrétní formální jazyky, které slouží k vyvracení obecného tvrzení. Protipříklady mohou být zařazeny do Chomského hierarchie, viz následující obrázek.
Counterexamples are concrete formal languages that are used for disproving universal statement. Counterexamples can be located in Chomsky hierarchy as shown in next picture.
Výsledkem operace nad konkrétními jazyky je vždy konkrétní jazyk. V důkazech se například často používá prázdná množina (∅), díky zjednodušení výsledku operace.
Result of operation on concrete languages is always a concrete language. In proofs, empty set (∅) is often used because of simplified result of operation.
Tento typ dedukčního kroku musí obsahovat právě jeden předpoklad a závěr. Krok slouží k odvozování na základě vlastností Chomského hierarchie gramatik a jazykových tříd. Validními kroky jsou například:
Subset step contains exactly one premise and a conclusion. Step is based on properties of Chomsky hierarchy of grammars and language classes. For example, valid steps are:
Za tento typ kroku lze považovat i odvození obecného tvrzení z tvrzení o konkrétním jazyku, například:
Same step is used for deducing concrete statement from language statement, such as:
Dedukční krok musí obsahovat právě jeden předpoklad a závěr. Krok pracuje pouze s názvem jazyka, který porovnává v předpokladu a v závěru. Případy, kdy se jazyky rovnají, jsou reprezentovány v programu jako sada následujících pravidel, která platí pro libovolný jazyk ___.
Set equality step contains exactly one premise and a conclusion. Step works only with the name of language which is compared in the premise and in the conclusion. Cases when languages are equal are represented as a set of rules in the table. Rules can be applied to every language ___.
Nejdůležitějším krokem v důkazu bývá vytvoření jazyka aplikováním operace na dílčí jazyky. V některých z těchto kroků je nutné využít známých uzávěrových vlastností, například:
The most important step in proof can be application of an operation on languages. In some of these steps, it is necessary to use known closure properties:
V některých případech lze tento krok nad obecnými tvrzeními sestavit bez uzávěrové vlastnosti. Za ___ lze dosadit jazyk z libovolné třídy (avšak v rámci jednoho pravidla vždy ze stejné třídy).
In some cases, it is possible to create the step without closure property. Symbol ___ can be replaced with every language class (but replaced classes have to be same in a rule).
Podporované dedukční kroky s konkrétními jazyky jsou znázorněny v následující tabulce. Symbol ___ zde má obdobný význam.
Supported operation steps with concrete languages are listed in the table. Symbol ___ has similar meaning here.
V případech, ve kterých je některý z operandů libovolný a nezávisí na něm výsledek operace, není nutné předpoklad uvádět, například lze vytvořit kroky:
In some cases when some operand is not rellevant (result of operation does not depend on it), it is not necessary to used this premise in the step. For example, valid steps are:
Program vznikl roku 2017 jako bakalářská práce na Fakultě informatiky Masarykovy univerzity v Brně.
Application was created in 2017 as a bachelor thesis on the Faculty of Informatics, Masaryk University, Brno.