knowledge representation - rule based, first order logic

Hello everyone,
I am looking for a very powerful system for representing
knowledge using first order logic rules. Basically, a concept would be
represented by a set of rules (represented in first order logic).
There will be a rule based engine which would be able to do reasoning
on the knowledge base. I hope I am able to explain myself clearly
enough.

Are there any commercially/freely available systems out there that can
capture first order logic and also reasoning. I would prefer freely
available ones. Its for student projects.

I would like to give the system a set of first order triplets as
axioms and a set of deduction rules.
Given a theorem it should give a proof.

I need to do a prototype for some small domain like say, basic high
school algebra. I am hoping there are theorem proving systems or some
packages based on prolog etc which can help me do this in a few months
time.

Thanks for your help.

[ comp.ai is moderated ... your article may take a while to appear. ]
.

Relevant Pages
Loading