Publikace na Matematicko-fyzikální fakulta |
2009
Abstrakt
Automatické dokazování vět ve velkých teoriích používá často víc axiomů než lze efektivně zpracovat v operační paměti. Tato práce se věnuje způsobům přístupu k externím zdrojům axiomů pro dokazovací systém v logice prvního řádu.