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