Společnost AMD na veletrhu Computex 2024 představila (YouTube) mimo jiné nové série procesorů pro desktopy AMD Ryzen 9000 a notebooky AMD Ryzen AI 300.
OpenCV (Open Source Computer Vision, Wikipedie), tj. open source multiplatformní knihovna pro zpracování obrazu a počítačové vidění, byla vydána ve verzi 4.10.0 . Přehled novinek v ChangeLogu. Vypíchnout lze Wayland backend pro Linux.
Národní superpočítačové centrum IT4Innovations s partnery projektu EVEREST vydalo sadu open source vývojových nástrojů EVEREST SDK pro jednodušší nasazení aplikací na heterogenních vysoce výkonných cloudových infrastrukturách, zejména pro prostředí nabízející akceleraci pomocí FPGA.
Společnost Valve aktualizovala přehled o hardwarovém a softwarovém vybavení uživatelů služby Steam. Podíl uživatelů Linuxu aktuálně činí 2,32 %. Nejčastěji používané linuxové distribuce jsou Arch Linux, Ubuntu, Linux Mint a Manjaro Linux. Při výběru jenom Linuxu vede SteamOS Holo s 45,34 %. Procesor AMD používá 75,04 % hráčů na Linuxu.
Blíží se léto, chladiče topí, tranzistory se přehřívají, novinářům pomalu docházejí témata a nastává klasická okurková sezóna. Je tomu tak i mezi bastlíři? Na to se podíváme na Virtuální Bastlírně! Tentokrát se strahováci podívají na zoubek velmi slibně vypadajícímu open-source EDM projektu - ne, nejde o taneční hudbu, ale o elektroobrábění. Ukáží taky, jak vypadá starší cykloradar zevnitř nebo jak se testuje odolnost iPhonů.
… více »Společnosti Ticketmaster byla odcizena databáze s osobními údaji (jméno, adresa, telefonní číslo a část platebních údajů) 560 miliónů zákazníku. Za odcizením stojí skupina ShinyHunters a za nezveřejnění této databáze požaduje 500 tisíc dolarů [BBC].
Byla vydána nová stabilní verze 24.05 linuxové distribuce NixOS (Wikipedie). Její kódové označení je Uakari. Podrobný přehled novinek v poznámkách k vydání. O balíčky se v NixOS stará správce balíčků Nix.
Byla vydána nová verze 1.48.0 sady nástrojů pro správu síťových připojení NetworkManager. Novinkám se v příspěvku na blogu NetworkManageru věnuje Fernando F. Mancera. Mimo jiné se v nastavení místo mac-address-blacklist nově používá mac-address-denylist.
Před 25 lety, 31. května 1999, započal vývoj grafického editoru Krita (Wikipedie). Tenkrát ještě pod názvem KImageShop a později pod názvem Krayon.
Paní docentka Alena Lukasová, která tuto problematiku vyučuje na Ostravské univerzitě, velmi dobře vystihuje místa, kde zpomalit nebo kde podat praktický příklad.
Formální (také matematická) logika je vědní obor, který se snaží formalizovat okolní svět do takového tvaru, aby se s ním dalo dále pracovat (zejména sledovat dedukce - usuzování). Je zřejmé, že je nutno vše zjednodušit, a proto se zavádějí různé modely. Pro matematiky je velmi výhodná výroková (založená na dvouhodnotové pravdivosti - na rozdíl od fuzzy logiky), informatiky bude zajímat predikátová a klauzurní logika.
Po první kapitole, jež představuje úvod do znalostí a jejich reprezentace (vzhledem ke zbytku knihy je tato problematika brána dosti stručně), začíná první část knihy, která se zabývá výrokovou logikou. Hned po přečtení prvních stran jsem ke svému potěšení zjistil, že se jedná o formální studijní materiál (Definice - Věta - Důkaz, Definice - Věta - Důkaz). Další, co mě potěšilo, byla téměř naprostá shoda s výkladem docenta Bělohlávka, který mě základům matematické logiky učil.
Výroková logika je tou nejjednodušší variantou, její vyjadřovací síla je tudíž nejmenší. Každý výrok se pomocí logických spojek snažíme ve správném tvaru zapsat do formulí a ty pak dále studovat. Můžeme zjišťovat pravdivost formule při jejím ohodnocení, zkoumat splnitelnost (tautologie, kontradikce) formule (například tabulkovou metodou) nebo převádět formuli do normálních tvarů (konjunktivní, disjunktivní). Právě jsem shrnul téma druhé kapitoly.
Třetí kapitola zavádí důležitý pojem důkazu ve výrokové logice, který poskytuje mechanizmus (ať už přímý nebo nepřímý) odvození platnosti (tautologičnosti) formule. Na základě znalostní báze (axiomů) a rezolučního odvozovacího pravidla jsme schopni rozhodnout o platnosti, aniž bychom studovali ohodnocení formule. V závěru kapitoly je pak popsána tablová důkazová metoda.
Velice důsledně jsou popsány tři nejpoužívanější axiomatické systémy (Gentzenovský, Klauzulární a Hilbertovský). Věnuje se jim čtvrtá kapitola. Při konstrukci důkazů je nutno získat trochu cviku, a proto je v této kapitole velké množství příkladů. Máme za sebou zhruba třetinu knihy, nyní se budeme věnovat predikátové logice.
Predikátová logika je svým způsobem rozšířením logiky výrokové. Do korektně vytvářených formulí definice přidává nové symboly (kvantifikátory) - generalizační a existenční, proměnné (které zde obsahují prvky z univerza), konstanty, funktory a predikátové symboly. Vyjadřovací schopnost predikátové logiky je mnohem vyšší, daní je pak složitější práce s takto utvořenými formulemi. Druhá třetina knihy se nese v podobném duchu, jako u výrokové logiky. Týká se ale logiky predikátové.
Asi nejzajímavější je poslední třetina, která je věnována klauzurní logice, jež je přechodovým stupněm mezi logikou predikátovou a logickým programovacím v jazyku PROLOG. Po přečtení kapitoly čtenář získá základní znalosti, jak funguje interpret jazyka PROLOG, kapitola však není návodem, jak v tomto jazyce programovat. V operačním systému Linux však funguje mnoho implementací PROLOGU (například GNU PROLOG), a tak není problém si vše vyzkoušet na počítači.
Knihu mohu jen doporučit. Nejen, že je profesionálně zpracovaná, ale spolu s bezchybnou a úhlednou sazbou je radost ji číst. Na závěr bych rád vyřešil jednu jednoduchou úlohu z první části knihy (výroková logika), abyste si mohli udělat obrázek, o čem tady celou dobu píši.
Převeďte formuli do konjunktivní normální normy c -› (a v b):
Řešení:
Vidíme, že řešení (6) je zároveň také v úplné disjuntní normální formě.
Název | Formální logika v umělé inteligenci |
Autoři | Alena Lukasová |
Vydal | Computer Press |
ISBN | 80-251-0023-5 |
Datum vydání | 2003 |
Počet stran | 270 |
Doporučená cena | 199 Kč / 299 Sk |
Nástroje: Tisk bez diskuse
Tiskni Sdílej:
a | b | c | c -> (a v b) | ¬a ^ ¬b ^ c ---+---+---+--------------+------------- 0 | 0 | 0 | 1 | 0 0 | 0 | 1 | 0 | 1 0 | 1 | 0 | 1 | 0 0 | 1 | 1 | 1 | 0 1 | 0 | 0 | 1 | 0 1 | 0 | 1 | 1 | 0 1 | 1 | 0 | 1 | 0 1 | 1 | 1 | 1 | 0