Szerintem elsőrendű rezolúciós kalkulussal megoldható, csak azt nagyon nehéz programozni (viszont ha egyszer sikerül, akkor már egész jól fogsz tudni automatikusan tételeket bizonyítani).
Vannak mindenféle erre kihegyezett programnyelvek (talán pl. Prolog, bár annyira még nem másztam bele a dolgokba és azt hiszem, hogy az inkább szabályalapú következtetésre való.)
Ez persze nem sok minden, de ha tényleg érdekel a dolog, akkor keress rá a rezolúcióra, elég nagy irodalma van, biztos találsz hozzá neten dolgokat.

Encsé