Learning Search Control Knowledge for Equational Deduction

O lucrare de referință în domeniul teoriei demonstrației, această teză explorează o abordare inovatoare pentru învățarea heuristicilor de căutare eficiente în cadrul proverului de teoreme E, specializat în deducții ecuaționale. Prin reprezentarea deciziilor de căutare din căutările de dovezi de succes ca seturi de modele de clauze annotate, autorul deschide noi orizonturi în înțelegerea procesului de demonstrație. Utilizând metoda de învățare Term Space Mapping, lucrarea propune funcții de evaluare a heuristicilor, esențiale pentru evaluarea consecințelor potențiale.

Rezultatele experimentale obținute cu sistemul extins E/TSM subliniază eficiența acestei abordări, demonstrând contribuții semnificative în domeniu. În plus, teza include o calcul de superpoziție extins și o descriere detaliată a procedurii de dovadă, precum și a implementării unui prover de teoreme ecuaționale de ultimă generație. Această lucrare se dovedește a fi un ghid esențial pentru cercetătorii și practicienii din domeniul inteligenței artificiale și al logicii formale.