Abstrakt
Do tableau kalkulu (konkrétně do jádra systému leanCoP) bylo přidáno pravděpodobnostní řízení založené na strojovém učení znalostí. V typickém matematickém nastavení při řešení mnoha problémů v rozsáhlých komplexních teoriích se využívá strojově naučených znalostí z předchozích úspěšných řešení pro řízení dokazování v duchu systému MaLARea.
Zatímco systém MaLaRea je založen na výběru axiomů aniž by došlo ke změnám v použitých systémech pro dokazování vět, v systému MaLeCoP je strojově naučené řízení integrováno přímo uvnitř dokazovače. Díky této integraci je dosaženo mnohem lepší interakce mezi naučenou znalostí a jejím použitím.
Toto přináší zajímavé možnosti pro další konstrukce, jako jsou trénování samostatně se učících umělo-inteligentních matematických expertů nad velkými matematickými knihovnami. Některé z takovýchto konstrukcí jsou v článku popsány.