I do maths/computer science for a living (research into automated theorem proving) ...
Are folks still using Prolog for those kinds of things? I started my software career with the LP crowd in the mid '80s.
The prover I work on is programmed in SML, a bit of a learning curve for me whose background was FORTRAN and c. I spent some time teaching Prolog - it is fun especially when you use it backwards (eg give the string concatenation function an output string and it finds all the pairs of substrings). There was a very small theorem prover written in Prolog called Lean TAP by
Beckert and Posegga in 1994:
the entire code is here:
prove((A,B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,[B|UnExp],Lits,FreeV,VarLim).
prove((A;B),UnExp,Lits,FreeV,VarLim) :- !,
prove(A,UnExp,Lits,FreeV,VarLim),
prove(B,UnExp,Lits,FreeV,VarLim).
prove(all(X,Fml),UnExp,Lits,FreeV,VarLim) :- !,
\+ length(FreeV,VarLim),
copy_term((X,Fml,FreeV),(X1,Fml1,FreeV)),
append(UnExp,[all(X,Fml)],UnExp1),
prove(Fml1,UnExp1,Lits,[X1|FreeV],VarLim).
prove(Lit,_,[L|Lits],_,_) :-
(Lit = -Neg; -Lit = Neg) ->
(unify(Neg,L); prove(Lit,[],Lits,_,_)).
prove(Lit,[Next|UnExp],Lits,FreeV,VarLim) :-
prove(Next,UnExp,[Lit|Lits],FreeV,VarLim).
Don't ask me to explain its workings! Most of the fast first-order-logic theorem provers I've worked with have been written in C for speed and to allow complex indexing techniques to be used.