Automated theorem proving
Automatizované dokazování teorémů (ATP) je oblast výpočetní logiky a umělé inteligence, která se zabývá automatickým dokazováním matematických tvrzení pomocí algoritmů a počítačových programů. Cílem ATP je ověřit platnost logických propozic nebo najít důkazy pro tvrzení, která lze formulovat v přísně definovaných formálních systémech. ATP využívá různé metody, jako jsou rezoluce, dominantní strategie a další logické techniky, k prokazování tvrzení v různých oblastech matematiky a informatiky. Systémy automatizovaného dokazování se široce používají v oblasti ověřování softwaru, formální verifikace, umělé inteligence a dalších aplikací, kde je důležitá rigoróznost a přesnost důkazů. V současnosti existuje řada různých ATP systémů, které se liší ve svých metodách a přístupech k řešení problémů.