Podobieństwo zdań(logika)

Witam,
Jestem w trakcie pisania programu do dowodzenia twierdzeń. Już sporo napisałem ale są mi potrzebne pewne wskazówki chociaż do dalszej pracy.
Problem jest taki:
mamy pięć aksjomatów:

1. (pvp)=>p
2. p=>(qvp)
3. (pvq)=>(qvp)
4. (pv(qvr))=>(qv(pvr))
5. (p=>q)=>((rvp)=>(rvp))
   procedura ma stwierdzić do którego aksjomatu jest podobne wprowadzone twierdzenie.
   np. (~pvp)=>~p jest podobne do pierwszego aksjomatu
   Człowiek podobieństwo widzi natychmiastowo. Niestety z komputerem już tak łatwo nie jest. Podobnych przykładów mógłbym wymieniać w nieskończoność.
   Chciałbym aby ktoś chociaż podał mi jak to zrobić po ludzku - nie musicie pisać nawet kodu, aby mi pomóc.
   Inaczej tego wytłumaczyć nie potrafię.
   W programie operuje na stringach.

dowodzenia twierdzen Tak nie robimy :
należy rozwalić wszysko na CNF
http://www.zgapa.pl/zgapedia/Koniunkcyjna_posta%C4%87_normalna.html
lub DNF
http://www.zgapa.pl/zgapedia/Dysjunkcyjna_posta%C4%87_normalna.html

Mamy Twierdzenie
(p=>q)=>((rvp)=>(rvp))

Zwijamy Atomy od najbardziej zewnetrznych nawiasow

A=>B
przekształcamy postać

~A v B

~(p=>q)V((rvp)=>(rvp))

~(pvq)v((rvp)v(rvp))

(p^~q)v((~r~p)v(rvp))

(p^{~q)v((rvp v ~r)} (rvp v~p)) // coś lub (1 ^1 ) =1 prawda

oczywiscue to jescze nie jest wlasciwa postac ale Mozna to robic dalej .

mozesz to zrobic tak że kazda litera alfabetu to atom a
każdy wiekszy atom to kolejne nawiasy ikazdy starasz sie rozdzielic