Wikipédia:Tudakozó/Archívum/2018-05-11

A Tudakozó főoldala • Én szeretnék választ adni! •  Archívum •  Eszmecsere a válaszadó önkéntesek között• Válaszadó sablonok •  TUGYIK

Egy szótárba illő kérdésnek, a szavak értelmezésének inkább a Wikiszótárban nézz utána.
A Wikipédia Tudakozójának önkéntesei vagyunk, és enciklopédiába, lexikonba való témákban igyekszünk választ adni. Megkérünk, hogy először a Wikipédia automatizált belső keresőjével próbáld a választ megkeresni, és csak ha ott nem találtad meg, akkor kattints ide, és tedd fel nekünk a kérdésedet!

A kérdésed (nem a válasz még!) egy-két perc elmúltával a mai kérdéseket tartalmazó lap alján fog látszani.
(Ha mégsem látszana, akkor próbáld meg a lapot a böngésződben frissíteni.)
Kérünk, hogy legyél türelemmel – itt mindenki a szabad idejét fordítja arra, hogy a segítségedre legyen.
Esetleg csak holnap, holnapután akad valaki, aki válaszolni tud neked, sőt néha még később írnak be egy választ a már archivált lapra.
Ha a mai lapot később keresed, ezt írd be a keresőablakba: Wikipédia:Tudakozó/Archívum/2024-04-24, vagy keresd az Archívumban.

A legutóbbi pár nap:

Wikipédia:Tudakozó/Archívum/2024-04-20 Négy napja

Wikipédia:Tudakozó/Archívum/2024-04-21 Három napja

Wikipédia:Tudakozó/Archívum/2024-04-22 Tegnapelőtt

Wikipédia:Tudakozó/Archívum/2024-04-23 Tegnap

Wikipédia:Tudakozó/Archívum/2024-04-24 Ma

2018. 5. 8. « 2018. 5. 9. « 2018. 5. 10. « 2018. 5. 11. » 2018. 5. 12. » 2018. 5. 13. » 2018. 5. 14.

= kezelése automatikus tételbizonyításnál

Valaki bebizonyította, hogy a konstruktív bizonyítás ekvivalens a hagyományossal, aminél végtelen sok axióma van. A hagyományosnak sajnos nem tudom a nevét, elméletinek hívom. Az angol Wikipédiában csak általánosan láttam leírva mi az a konstruktív bizonyítás, nekem viszont konkrét lépések kellenek, hogy a számítógép meg tudja csinálni. A konstruktív bizonyítás lépései érdekelnek: weboldal, könyv (szerző, cím), vagy akármi. Könyvet előbb megpróbálom megkeresni az interneten. Gondolom angolul van, majd szótárt használok. Magyarul lenne a legjobb, de még eszpertantóul is jobb mint angolul: a nyelvtant nagyrészt tudom, táblázatkezelőben megnyitható táblázatban megvan az összes szó amit középfokú nyelvvizsgára tudni kell, csak 200-300 fordul elő ilyen szakszövegben, azokat megtanulom, a többihez használok szótárt. Angolul a szókat értem, de köztük a kapcsolatokat nehezen: ez a nyelvtantól függ, tehát amit magyarul toldalékkal fejezünk ki, azt nehezen értem.

Az alap lépéseket gondolom rezolúcióval és egyesítéssel kezeli, ez rendben is van. Engem leginkább a beépített = kezelése érdekelne, mert az is végtelen sok axióma. Logikai kifejezések között rezolúcióval kezelhető, de 1. és 2. rendű kifejezések között is kell, ezt a Prolog se kezeli. Az = tranzitivitása még könnyű, de például (A=B ∈ H) esetén, ahol H konstans, DNF-ben (A=B ∧ A∈X ∧ B∈Y) a leírása, ahol X∩Y = H, így végtelen sok leírása van, jó elkerülni az összes előállítását. CNF-ben unióval kell metszet helyett. Ez normalizálással megoldható, hogy az egyikhez teszem az egész H-t, miatta a többi lépést módosítani kell. Színezés is kell: például x, y, z ∈ {a, b}, és kölcsönösen nem=-ek: ellentmondást kell észrevenni. Klóz literáljai között és klózok között is kell színezés. Az is érdekelne hogy beépített ∈, <, ≤, +, -, *, /, egészre kerekítés, hatványozás, logaritmus-ra van-e módszere, nyilván hatványozásnál és logaritmusnál csak egy intervallumot ad hogy abban van az eredmény, nem pontosan adja meg. Ezek nagy 1. vagy 2. rendű kifejezés mélyén is lehetnek. Hatása csak úgy lehet, ha a kifejezés gyökerébe kerül a hatása, innen visszafele is lehetne menni, de ha végtelen sok értéket kellene végigpróbálni hozzá az nem jó, alul (a kifejezés mélyén) viszont kiderülhet melyik kell: felfele kiértékeléssel (a gyökér felé haladva) megkapjuk.

Az is érdekelne hogy 1. vagy 2. rendű-e, és lehetnek-e a kifejezés közepén is kötések, vagy ki kell emelni őket (Prenex normálalak, Skolem-függvények). Az is érdekelne hogy rezolúciónál irányítottan megy-e, hogy csak a kellő célhoz használható klózokat állítja elő, vagy az összeset. Köszönöm.

--2A01:36C:1400:6B7C:3CC2:CE91:ECD0:F2C4 (vita) 2018. május 11., 12:39 (CEST)

Válasz

• Az angol a programozás nélkülözhetetlen kommunikációs nyelve, sajátítsd el.
• Angol összefoglaló a témáról: en:Constructive proof
• A Konstruktív bizonyítás szabályai, 31 oldalas áttekintő: The rules of constructive reasoning - Rosalie Iemho, Utrecht University
• A programozási környezet részletei már annyira speciálisak, hogy aktív programozó matematikusok tudnak rá érdemben válaszolni, kérlek keress olyan fórumokat, ahol aktívan beszélgetnek, példa: https://prog.hu/cimkek/matematika/5
• Felsőfokú oktatási intézmények témában járatos kutatóit, kutatócsoportjait is megkeresheted a témáddal.

– Rodrigó ⇔ 2018. május 17., 15:52 (CEST)

Angol középfokúm van, de sokat felejtettem, iszonyatos nyögés volt a vizsga, beszédértésen csak tippeltem és bejött, így mentem át. Szótárral meg nyelvtan-könyvvel megy nehezen.

Az angol Wikipédiában az automatikus tételbizonyításnál en:Automated theorem proving írnak róla, nem a konstruktív bizonyításnál. Sajnos amit eddig láttam, az = kezelése említve se volt, amit belinkeltél abban sincs. Ezek miatt egyenlőre levettem hogy megválaszolva, főleg amiatt hogy automatikus tételbizonyítás néven vannak róla írva dolgok, nem konstruktív bizonyítás néven. Sajnos nem az = kezeléséről írnak. Egyébként köszönöm hogy megpróbáltál segíteni. Később megpróbálom a prog.hu-t, meg egyetemeket is esetleg.

2A01:36C:1400:2D70:3CC2:CE91:ECD0:F2C4 (vita) 2018. május 17., 21:49 (CEST)