Diky, tohle jsem v tom proveru nemel energii hledat. Kazdopadne hlasim, ze pred chvili mi Vyskocil dal zapocet (reseni jsem odevzal presne takove, jake jsem popsal v prvni prispevku).jirka_v píše:Pro inspiraci jeste prikladam vstupni soubor pro prover9 k dokazani (v7) v Hilbertove systemu.
Zápočtový příklad - Vyskočil
- Lukas Mach
- Matfyz(ák|ačka) level III
- Příspěvky: 261
- Registrován: 28. 3. 2006 17:08
- Typ studia: Informatika Bc.
- Bydliště: Praha a Kladno
- Kontaktovat uživatele:
Re: iny druh domacej
For every epsilon, there is delta.
Where is my delta?
Where is my delta?
Re: iny druh domacej
No, zjistil jsem toho vícero: http://fitelson.org/ar.htmlClassical Sentential Logic --- In the Sheffer Stroke (D):zoufalec píše:Napsal by si sem prosím jak vypadal ten vstup pro proover a jak si to pak přepsal? + co na to případně vyskočil, když chce i zdroják pokud to budem řešit kompem. Mám velmi podobnej úkol. Předem dík
D je sheffler stroke (NAND)
Nicoduv a Lukasiewiczuv system s jedinym axiomem a jednou logickou spojkou vypada takhle:
Ja mam k dispozici dane odvozovaci pravidlo a axiom P(d(d(x,d(y,z)),d(d(x,d(z,y)),d(d(u,y),d(d(x,u),d(x,u)))))) jez se zasobnikove zapise jako DDpDqrDDpDrqDDsqDDpsDps - podezrele se to podoba predchozim... ale vcelku jsem si krome zajimaveho pocteni tolik nepomohl, narozdil od nekoho kdo mel k tomuhle systemu najit semantiku (mam u tebe aspon pivo ). Porad jeste z toho musim dokazat tu megaformuli s Proverovskym dlouhym dukazem ktery se prepisuje do formalni logiky dosti nepohodlne - nejake zkusenosti anyone?[/quote]In 1917, Nicod [21] showed3 that the following 23-symbol formula (in Polish notation) is a single axiom for classical sentential logic (D is interpreted semantically as NAND, i.e., the Sheffer stroke):
DDpDqrDDtDttDDsqDDpsDps
The only rule of inference for Nicod's single axiom system is the following, somewhat odd, detachment rule for D:
From DpDqr and p, infer r.
Lukasiewicz [7] later showed that the following substitution instance (t/s) of Nicod's axiom (N) would suffice:
DDpDqrDDsDssDDsqDDpsDps
Lukasiewicz's student Mordchaj Wajsberg [37] later discovered the following organic4 23-symbol single axiom for D:
DDpDqrDDDsrDDpsDpsDpDpq
Lukasiewicz later discovered another 23-symbol organic axiom:
DDpDqrDDpDrpDDsqDDpsDps
We have discovered many new 23-symbol single axioms, some of which are organic and have only 4 variables, e.g.,
DDpDqrDDpDqrDDsrDDrsDps
We can now report that the shortest single axioms for these Sheffer Stroke systems contain 23 symbols. No shorter axioms exist.
Re: Zápočtový příklad - Vyskočil
prosím prosím, napište sem někdo jak se cvičící staví k tomu Proveru? Neumím si moc představit jak to řešit bez něj... a potřebuji to velice rychle odevzdat...