Stránka 2 z 2

Re: iny druh domacej

Napsal: 6. 9. 2007 15:33
od Lukas Mach
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).

Re: iny druh domacej

Napsal: 8. 9. 2007 01:58
od keff
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]

Napsal: 12. 9. 2007 20:11
od keff
Tak to mam, jupiii :)

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

Napsal: 29. 9. 2008 00:56
od panther
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...