Automatyczne rozumowanie, mechanizacja rozumowania – część reprezentacji wiedzy i rozumowania oraz metalogiki zajmująca się badaniem aspektów rozumowania. Badanie automatycznego rozumowania pozwala tworzyć modele w formie programów komputerowych, które są w stanie rozumować całkowicie lub prawie całkowicie automatycznie. Mimo że zautomatyzowane rozumowanie jest uważane za poddziedzinę sztucznej inteligencji, ma ono również powiązania z teorią informatyki i filozofią.
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ę.
Narzędzia i techniki automatycznego rozumowania obejmują klasyczną logikę, logikę rozmytą, wnioskowanie bayesowskie i wiele mniej formalnych technik ad hoc.
Systemy dowodowe 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.
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).
Aplikacje Oprócz zagadnienia dowodzenia twierdzeń w matematyce, automatyczne rozumowanie ma zastosowanie w informatyce w weryfikowaniu implementacji protokołów kryptograficznych czy innych usług i dziedzinie sztucznej inteligencji w przeciwdziałaniu halucynacjom.
Zobacz też automatyczne dowodzenie twierdzeń analiza programów (informatyka) kazuistyka model rozumujący rozumowanie abdukcyjne
Przypisy
Kategoria:Automatyczne dowodzenie twierdzeń Kategoria:Automatyczne rozumowanie