Programming language for working with axioms

Question

edit: Prolog is the answer.

Answer 1

Prolog is good for handling axioms. There is a open source object-oriented extension of prolog at sourceforge.net:

http://sourceforge.net/projects/oopl/

Answer 2

I believe the type system of the Fortress Programming Language works in some way similar to what you describe. It uses an Object-Oriented Type System with Generic Traits to describe e.g. Algebraic Properties of Operators (like Associativity, Commutativity, Distributivity, Identity, Symmetry, One-Element, Zero-Element and so on). It needs to know all these in order to automatically distribute computations across nodes in a cluster.