[Agda] ring solver

[Nils Anders Danielsson]

On 2010-03-13 12:34, Ruben Henner Zilibowitz wrote:
> I've been trying out the ring solver in Algebra.RingSolver. I've
> noticed it uses "almost commutative rings" instead of actual rings. Is
> the code here able to deal with proper rings such as the integers, or
> only semirings such as the natural numbers?

The ring solver can handle both commutative rings and commutative
semirings, see Algebra.RingSolver.AlmostCommutativeRing. The idea to use
"almost commutative rings" comes from a paper by Grégoire and Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq.

> I've actually tried it on the full integers and it just eats up all my
> computer's memory and never produces any answer.

The ring solver may simply be too inefficient for your example.

--
/NAD