Optymalizacja dowodu syntaktycznego

[foundofmath]

Czy są jakieś metody optymalizacji dowodu syntaktycznego ze względu na liczbę formuł ciągu dowodowego jak również złożoność formuł występujących w dowodzie (najkrótszy dowód oraz dowód którego formuły nie przekraczają najmniejszej możliwej złożoności; w każdym z przypadków przy danym układzie aksjomatów)? Gdzie można o tym poczytać?