Automatyczne rozumowanie
Automatyczne rozumowanie[1], mechanizacja rozumowania[2][3] – część reprezentacji wiedzy i rozumowania oraz metalogiki zajmująca się badaniem aspektów rozumowania[4]. Badanie automatycznego rozumowania pozwala tworzyć modele w formie programów komputerowych, które są w stanie rozumować całkowicie lub prawie całkowicie automatycznie[4]. Mimo że zautomatyzowane rozumowanie jest uważane za poddziedzinę sztucznej inteligencji, ma ono również powiązania z teorią informatyki i filozofią[4].
Najbardziej rozwiniętą częścią automatycznego rozumowania jest automatyczne dowodzenie twierdzeń i systemami wspomagającymi dowodzenie twierdzeń. Prowadzono również liczne prace nad rozumowaniem przez analogię, wykorzystując indukcję i abdukcję[5].
Narzędzia i techniki automatycznego rozumowania obejmują klasyczną logikę, logikę rozmytą, wnioskowanie bayesowskie i wiele mniej formalnych technik ad hoc.
Systemy dowodowe
[edytuj | edytuj kod]- HOL Light
- HOL Light, napisany w OCamlu, został zaprojektowany tak, aby miał prostą, przejrzystą i logiczną składnię oraz pozwalał na przejrzystą implementację. Może być używany jako asystent dowodzenia dla klasycznej logiki wyższego rzędu[6].
- Coq
- Coq to kolejny zautomatyzowany asystent dowodzenia Potrafi on automatycznie wyodrębniać programy wykonywalne ze specyfikacji do kodu źródłowego Objective CAML lub Haskell. Właściwości, programy i dowody są formalizowane w tym samym języku o nazwie Calculus of Inductive Constructions (CIC)[7].
Aplikacje
[edytuj | edytuj kod]Oprócz zagadnienia dowodzenia twierdzeń w matematyce, automatyczne rozumowanie ma zastosowanie w informatyce w weryfikowaniu implementacji protokołów kryptograficznych czy innych usług[8] i dziedzinie sztucznej inteligencji w przeciwdziałaniu halucynacjom[9].
Zobacz też
[edytuj | edytuj kod]Przypisy
[edytuj | edytuj kod]- ↑ G. Kochański, Metody poszukiwania i selekcji informacji, „Zeszyty Naukowe Wydziału Elektrotechniki i Automatyki Politechniki Gdańskiej”, Nr 22, 2006, s. 99–104, ISSN 1425-5766 [dostęp 2025-05-04] (pol.).
- ↑ Witold Marchiszewski, Dlaczego nie każde rozumowanie da się zmechanizować? [online], calculemus.org, 2000 [dostęp 2025-05-04].
- ↑ Kazimierz Trzęsicki, Leibnizjańskie inspiracje informatyki, „Filozofia Nauki”, 14 (3 (55)), 2006, s. 21–48, ISSN 1230-6894 [dostęp 2025-05-04] (pol.).
- ↑ a b c Frederic Portoraro, Automated Reasoning, Edward N. Zalta, Uri Nodelman (red.), wyd. Spring 2025, Metaphysics Research Lab, Stanford University, 2025 [dostęp 2025-05-04].
- ↑ Gilles Defourneaux, Nicolas Peltier, Analogy and abduction in automated deduction [online], www.semanticscholar.org, 1997 [dostęp 2025-05-04].
- ↑ John Harrison, HOL Light: an overview [online], 2010 (ang.).
- ↑ A Tour of Rocq · Rocq Documentation [online], Rocq [dostęp 2025-05-04] (ang.).
- ↑ An unexpected discovery: Automated reasoning often makes systems more efficient and easier to maintain | AWS Security Blog [online], aws.amazon.com, 17 października 2024 [dostęp 2025-05-04] (ang.).
- ↑ Belle Lin, Why Amazon is Betting on ‘Automated Reasoning’ to Reduce AI’s Hallucinations, „Wall Street Journal”, 5 lutego 2025, ISSN 0099-9660 [dostęp 2025-05-04] (ang.).