Zápočtový příklad - Vyskočil

Re: iny druh domacej

Příspěvekod Lukas Mach » 6. 9. 2007 14:33

jirka_v píše:Pro inspiraci jeste prikladam vstupni soubor pro prover9 k dokazani (v7) v Hilbertove systemu.

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).
For every epsilon, there is delta.
Where is my delta?
Uživatelský avatar
Lukas Mach
Matfyz(ák|ačka) level III
 
Příspěvky: 261
Registrován: 28. 3. 2006 16:08
Bydliště: Praha a Kladno

Re: iny druh domacej

Příspěvekod keff » 8. 9. 2007 00:58

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


No, zjistil jsem toho vícero: http://fitelson.org/ar.htmlClassical Sentential Logic --- In the Sheffer Stroke (D):

D je sheffler stroke (NAND)

Nicoduv a Lukasiewiczuv system s jedinym axiomem a jednou logickou spojkou vypada takhle:


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.


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]
keff
Matfyz(ák|ačka) level I
 
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Příspěvekod keff » 12. 9. 2007 19:11

Tak to mam, jupiii :)
keff
Matfyz(ák|ačka) level I
 
Příspěvky: 28
Registrován: 24. 1. 2006 19:17

Re: Zápočtový příklad - Vyskočil

Příspěvekod panther » 28. 9. 2008 23:56

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...
panther
Matfyz(ák|ačka) level I
 
Příspěvky: 7
Registrován: 23. 1. 2006 21:51

Předchozí

Zpět na 2007

Kdo je online

Uživatelé procházející toto fórum: Žádní registrovaní uživatelé a 1 návštěvník

cron