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]